fromAffine_some_ne_zero — Mathlib

English

If a matrix-initial point is nonsingular, then its image in affine coordinates is given by the corresponding affine point.

Русский

Если точка задана как ненонсиглярная в матричной форме, её афинные координаты соответствуют аффинной точке.

LaTeX

$$$ (W.Nonsingular (Matrix.vecCons X (Matrix.vecCons Y (Matrix.vecCons 1 Matrix.vecEmpty)))) \Rightarrow toAffine W (Matrix.vecCons X (Matrix.vecCons Y (Matrix.vecCons 1 Matrix.vecEmpty))) = "affinePoint" $$$

Lean4

theorem fromAffine_some_ne_zero [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) : fromAffine (.some h) ≠ 0 :=
  mk_ne_zero <| (nonsingularLift_some ..).mpr h

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