English
If P is equivalent to Q under the Weierstrass Jacobian equivalence, then their affine images coincide.
Русский
Если P эквивалентен Q по эквивалентности Якобиана на кривой Вейерштрасса, то их аффинные образы совпадают.
LaTeX
$$$P \\approx Q \\Rightarrow toAffine(W, P) = toAffine(W, Q)$$$
Lean4
theorem toAffine_smul (P : Fin 3 → F) {u : F} (hu : IsUnit u) : toAffine W (u • P) = toAffine W P :=
by
by_cases hP : W.Nonsingular P
· by_cases hPz : P z = 0
· rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]
· rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]
simp only [smul_fin3_ext, mul_pow, mul_div_mul_left _ _ (hu.pow _).ne_zero, and_self]
· rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]
