equation_iff_nonsingular — Mathlib

English

If the discriminant Δ is nonzero, the equation is equivalent to nonsingularity.

Русский

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

LaTeX

$$equation_iff_nonsingular_of_Δ_ne_zero {x y : R} (hΔ : W.Δ ≠ 0) : W.Equation x y ↔ W.Nonsingular x y$$

Lean4

theorem equation_iff_nonsingular [Nontrivial R] [W.IsElliptic] {x y : R} :
    W.toAffine.Equation x y ↔ W.toAffine.Nonsingular x y :=
  W.toAffine.equation_iff_nonsingular_of_Δ_ne_zero <| W.coe_Δ' ▸ W.Δ'.ne_zero

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