Commit 2024-06-26 12:03 53e093f0

feat(EllipticCurve): lemmas in Jacobian coordinates (#13846)

• equiv_iff_eq_of_Z_eq: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal.
• nonsingular_iff_of_Z_ne_zero: a lemma deleted in an earlier PR for no reason, now restored.
• addXYZ_self: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0).
• addXYZ_neg: the addition formula applied to a point representative and its negation yields a representative of the point at infinity.
• two trivial lemmas fromAffine_ne_zero and comp_fin3.
• a series of map lemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms.