### Abstract

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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Related publications

- Hales, T., & Raya, R. (2020). Formal Proof of the Group Law for Edwards Elliptic Curves. Lecture Notes in Computer Science, 254–269. https://doi.org/10.1007/978-3-030-51054-1_15

### Session Edwards_Elliptic_Curves_Group

- Edwards_Elliptic_Curves_Group

## Cite

×

Edwards_Elliptic_Curves_Group-AFP

    @article{Edwards_Elliptic_Curves_Group-AFP,
      author  = {Rodrigo Raya},
      title   = {Group Law of Edwards Elliptic Curves},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Edwards_Elliptic_Curves_Group.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Mar 1, 2023 : Isabelle2022