mk_ne_zero — Mathlib

English

Same nonzero condition for the quotient representative arising from a nonsingular lift of [X,Y,1].

Русский

Повторение условия не нуля для представителя в стойке тождества, полученного из [X,Y,1].

LaTeX

$$$ (W'.NonsingularLift \langle [X,Y,1] \rangle) \Rightarrow (mk h \neq 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

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