nonsingularLift_zero — Mathlib

English

If R is nontrivial, then the lifted nonsingularity of the vector [1,1,0] is true on W'.

Русский

Если R является неприводимым (не нулевым) коммутативным кольцом, то подъём без сингулярности векторa [1,1,0] на W' истинен.

LaTeX

$$$$W'\\mathrm{NonsingularLift}(\\overline{[1,1,0]})$$$$

Lean4

theorem nonsingularLift_zero [Nontrivial R] : W'.NonsingularLift ⟦![1, 1, 0]⟧ :=
  nonsingular_zero

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