nonsingular_zero — Mathlib

English

Nonsingularity at (x,y) is equivalent to nonsingularity of the curve after a standard variable change, at (0,0).

Русский

Невырожденность в точке (x,y) эквивалентна невырожденности кривой после стандартного замещения переменных в точке (0,0).

LaTeX

$$nonsingular_iff_variableChange : ∀ {W x y}, W.Nonsingular x y ↔ (VariableChange.mk 1 x 0 y • W).toAffine.Nonsingular 0 0$$

Lean4

@[simp]
theorem nonsingular_zero : W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0) := by
  rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero, or_comm]

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