nonsingular_iff' — Mathlib

English

If the discriminant Δ is nonzero, the equation and nonsingularity are equivalent at a given point.

Русский

Если дискриминант Δ ≠ 0, то уравнение и невырожденность эквивалентны в заданной точке.

LaTeX

$$nonsingular_iff_nonsingular_of_Δ_ne_zero : ∀ {x y}, Δ W ≠ 0 → W.Equation x y ↔ W.Nonsingular x y$$

Lean4

theorem nonsingular_iff' (x y : R) :
    W.Nonsingular x y ↔
      W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) :=
  by rw [Nonsingular, equation_iff', evalEval_polynomialX, evalEval_polynomialY]

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