English
Let W be a Weierstrass curve and P a nonsingular projective point on W. Then the affine image of the negation of P is the negation of the affine image of P: toAffine(W, W.neg P) = - toAffine(W, P).
Русский
Пусть W — кривая Вейерштрасса, а P — ненонсигулярная проектная точка на W. Тогда аффинное образе противоположной точки равняется противоположному образу самой точки: toAffine(W, W.neg P) = -toAffine(W, P).
LaTeX
$$$\\operatorname{toAffine}(W, W\\neg P) = -\\operatorname{toAffine}(W, P)$$$
Lean4
theorem toAffine_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : toAffine W (W.neg P) = -toAffine W P :=
by
by_cases hPz : P z = 0
·
rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg, toAffine_zero,
toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]
·
rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz,
toAffine_some <| (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]
