toAffine_of_equiv — Mathlib

English

A variant of the equivalence invariance for the affine map on projective points.

Русский

Еще одна версия инвариантности афинного отображения относительно эквивалентности точек.

LaTeX

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

Lean4

theorem toAffine_of_equiv {P Q : Fin 3 → F} (h : P ≈ Q) : toAffine W P = toAffine W Q :=
  by
  rcases h with ⟨u, rfl⟩
  exact toAffine_smul Q u.isUnit

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