toAffine_smul — Mathlib

English

Continuation: equivalence of finite coordinate representations preserves the affine image.

Русский

Продолжение эквивалентности — сохранение афинного изображения.

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_div_mul_left _ _ hu.ne_zero, and_self]
  · rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

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