Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Group Law of Edwards Elliptic ...


view this post on Zulip Email Gateway (Mar 01 2023 at 16:21):

From: Tobias Nipkow <nipkow@in.tum.de>
Group Law of Edwards Elliptic Curves
Rodrigo Raya

This article gives an elementary computational proof of the group law for
Edwards elliptic curves. The associative law is expressed as a polynomial
identity over the integers that is directly checked by polynomial division.
Unlike other proofs, no preliminaries such as intersection numbers, B́ezout’s
theorem, projective geometry, divisors, or Riemann Roch are required.

https://www.isa-afp.org/entries/Edwards_Elliptic_Curves_Group.html

Enjoy!

smime.p7s


Last updated: Apr 19 2024 at 01:05 UTC