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 thanMvPolynomial
. IntroduceevalEval
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]
andY
fromEllipticCurve/Afffine.lean
to the new file. - Add two lemmas in
Affine.lean
that relatesnegPolynomial
andpolynomialY
, and two trivial lemmassome_ne_zero
andsome_eq_some_iff
. - Prove two affine formulas
addX_eq_subX_sub
andaddY_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 lemmamap_mapRingHom_eval_map_eval
; add a lemmaEquation.map
.