toAffine_some — Mathlib

English

If P and Q are equivalent under the quotient relation, their affine images coincide.

Русский

Если P и Q эквивалентны по отношению к эквивалентности двойного класса, их афинные изображения совпадают.

LaTeX

$$$ (P \approx Q) \Rightarrow toAffine W P = toAffine W Q $$$

Lean4

theorem toAffine_some {X Y : F} (h : W.Nonsingular ![X, Y, 1]) :
    toAffine W ![X, Y, 1] = .some ((nonsingular_some ..).mp h) := by
  simp only [toAffine_of_Z_ne_zero h one_ne_zero, fin3_def_ext, div_one]

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