mk_ne_zero — Mathlib

English

For a nonsingular lift h of a matrix representing a point, the corresponding mk h is nonzero.

Русский

Для несингулярного подъема h, представленного матрицей точки, соответствующий mk h не равен нулю.

LaTeX

$$mk h ≠ 0$$

Lean4

theorem mk_ne_zero [Nontrivial R] {X Y : R} (h : W'.NonsingularLift ⟦![X, Y, 1]⟧) : mk h ≠ 0 :=
  (not_equiv_of_Z_eq_zero_right one_ne_zero rfl).comp <| Quotient.eq.mp.comp Point.ext_iff.mp

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