Commit 2024-06-26 10:10 7ea51917

View on Github →

feat(EllipticCurve): affine formulas and bivariate polynomial lemmas (#13845)

  • Create a new file for materials about bivariate polynomials developed using R[X][X] rather than MvPolynomial. Introduce evalEval for evaluation at a point (x,y) on the plane, and use it in Affine.lean and Jacobian.lean.
  • Move the notations R[X][Y] and Y from EllipticCurve/Afffine.lean to the new file.
  • Add two lemmas in Affine.lean that relates negPolynomial and polynomialY, and two trivial lemmas some_ne_zero and some_eq_some_iff.
  • Prove two affine formulas addX_eq_subX_sub and addY_sub_negY which are crucial for the development of division polynomials.
  • Golf the definition of addition of rational points and subsequent lemmas, including two proofs in Group.lean.
  • Remove eval_polynomial(X,Y) lemmas in favor of bivariate polynomial lemma map_mapRingHom_eval_map_eval; add a lemma Equation.map.

Estimated changes