toAffine_neg — Mathlib

English

The affine image of the negation of a point is the negation of the affine image.

Русский

Аффинное образующее точку отрицания равно отрицанию её аффинного образа.

LaTeX

$$$ toAffine(W, W.neg P) = - 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 hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_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]

Похожие утверждения