nonsingular_zero — Mathlib

English

For a nontrivial base ring R, the Weierstrass projective curve W′ is nonsingular at the point represented by the vector [0,1,0].

Русский

При ненулевом основании R кривая Вейершраса в проекционной модели несингулярна в точке, представленной вектором [0,1,0].

LaTeX

$$$[\\text{Nontrivial } R] \\Rightarrow W'.Nonsingular\\bigl(\\begin{pmatrix}0 \\\\ 1 \\\\ 0\\end{pmatrix}\\bigr)$$$

Lean4

theorem nonsingular_zero [Nontrivial R] : W'.Nonsingular ![0, 1, 0] :=
  by
  simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]
  exact fun h => one_ne_zero <| by linear_combination (norm := ring1) h.right

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