feat(AlgebraicGeometry/EllipticCurve/*): some missing lemmas (#22601)

Add the simple lemmas `polynomial_relation` and `Equation.baseChange` that are present in some coordinate files but missing in others, and fix some `evalEval` names based on standard naming conventions.

Author: Multramate

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -335,10 +335,12 @@ lemma negY_negY (x y : R) : W'.negY x (W'.negY x y) = y := by
   simp only [negY]
   ring1
 
-lemma eval_negPolynomial (x y : R) : W'.negPolynomial.evalEval x y = W'.negY x y := by
+lemma evalEval_negPolynomial (x y : R) : W'.negPolynomial.evalEval x y = W'.negY x y := by
   rw [negY, sub_sub, negPolynomial]
   eval_simp
 
+@[deprecated (since := "2025-03-05")] alias eval_negPolynomial := evalEval_negPolynomial
+
 /-- The line polynomial `ℓ(X - x) + y` associated to the line `Y = ℓ(X - x) + y` that passes through
 a nonsingular affine point `(x, y)` on a Weierstrass curve `W` with a slope of `ℓ`.
 
@@ -473,13 +475,15 @@ lemma slope_of_X_ne {x₁ x₂ y₁ y₂ : F} (hx : x₁ ≠ x₂) :
     W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂) := by
   rw [slope, if_neg hx]
 
-lemma slope_of_Y_ne_eq_eval {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
+lemma slope_of_Y_ne_eq_evalEval {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
     W.slope x₁ x₂ y₁ y₂ = -W.polynomialX.evalEval x₁ y₁ / W.polynomialY.evalEval x₁ y₁ := by
   rw [slope_of_Y_ne hx hy, evalEval_polynomialX, neg_sub]
   congr 1
   rw [negY, evalEval_polynomialY]
   ring1
 
+@[deprecated (since := "2025-03-05")] alias slope_of_Y_ne_eq_eval := slope_of_Y_ne_eq_evalEval
+
 lemma Y_eq_of_X_eq {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
     (hx : x₁ = x₂) : y₁ = y₂ ∨ y₁ = W.negY x₂ y₂ := by
   rw [equation_iff] at h₁ h₂
@@ -739,10 +743,13 @@ lemma map_polynomial : (W'.map f).toAffine.polynomial = W'.polynomial.map (mapRi
   simp only [polynomial]
   map_simp
 
-lemma evalEval_baseChange_polynomial_X_Y :
+lemma evalEval_baseChange_polynomial :
     (W'.baseChange R[X][Y]).toAffine.polynomial.evalEval (C X) Y = W'.polynomial := by
   rw [map_polynomial, evalEval, eval_map, eval_C_X_eval₂_map_C_X]
 
+@[deprecated (since := "2025-03-05")] alias evalEval_baseChange_polynomial_X_Y :=
+  evalEval_baseChange_polynomial
+
 variable {x y} in
 lemma Equation.map {x y : R} (h : W'.Equation x y) : (W'.map f).toAffine.Equation (f x) (f y) := by
   rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean

@@ -32,6 +32,10 @@ group operations in `Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.le
  * `WeierstrassCurve.Jacobian.Nonsingular`: the nonsingular condition on a point representative.
  * `WeierstrassCurve.Jacobian.NonsingularLift`: the nonsingular condition on a point class.
 
+## Main statements
+
+ * `WeierstrassCurve.Jacobian.polynomial_relation`: Euler's homogeneous function theorem.
+
 ## Implementation notes
 
 All definitions and lemmas for Weierstrass curves in Jacobian coordinates live in the namespace
@@ -351,6 +355,13 @@ lemma eval_polynomialZ (P : Fin 3 → R) : eval P W'.polynomialZ =
   rw [polynomialZ_eq]
   eval_simp
 
+/-- Euler's homogeneous function theorem in Jacobian coordinates. -/
+theorem polynomial_relation (P : Fin 3 → R) : 6 * eval P W'.polynomial =
+    2 * P x * eval P W'.polynomialX + 3 * P y * eval P W'.polynomialY +
+      P z * eval P W'.polynomialZ := by
+  rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
+  ring1
+
 variable (W') in
 /-- The proposition that a Jacobian point representative `(x, y, z)` on a Weierstrass curve `W` is
 nonsingular.
@@ -532,6 +543,12 @@ lemma baseChange_polynomial : (W'.baseChange B).toJacobian.polynomial =
     MvPolynomial.map f (W'.baseChange A).toJacobian.polynomial := by
   rw [← map_polynomial, map_baseChange]
 
+variable {P} in
+lemma Equation.baseChange (h : (W'.baseChange A).toJacobian.Equation P) :
+    (W'.baseChange B).toJacobian.Equation (f ∘ P) := by
+  convert Equation.map f.toRingHom h using 1
+  rw [AlgHom.toRingHom_eq_coe, map_baseChange]
+
 variable {f} in
 lemma baseChange_equation (hf : Function.Injective f) :
     (W'.baseChange B).toJacobian.Equation (f ∘ P) ↔ (W'.baseChange A).toJacobian.Equation P := by

Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean

@@ -517,6 +517,12 @@ lemma baseChange_polynomial : (W'.baseChange B).toProjective.polynomial =
     MvPolynomial.map f (W'.baseChange A).toProjective.polynomial := by
   rw [← map_polynomial, map_baseChange]
 
+variable {P} in
+lemma Equation.baseChange (h : (W'.baseChange A).toProjective.Equation P) :
+    (W'.baseChange B).toProjective.Equation (f ∘ P) := by
+  convert Equation.map f.toRingHom h using 1
+  rw [AlgHom.toRingHom_eq_coe, map_baseChange]
+
 variable {f} in
 lemma baseChange_equation (hf : Function.Injective f) :
     (W'.baseChange B).toProjective.Equation (f ∘ P) ↔