Commit 2024-06-26 10:10 7ea51917

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.