equation_iff_nonsingular_of_Δ_ne_zero

English

Evaluating polynomialX at (0,0) gives -a4.

Русский

Значение polynomialX при (0,0) равно -a4.

LaTeX

$$evalEval_polynomialX_zero : W.polynomialX.evalEval 0 0 = -W.a₄$$

Lean4

theorem equation_iff_nonsingular_of_Δ_ne_zero {x y : R} (hΔ : W.Δ ≠ 0) : W.Equation x y ↔ W.Nonsingular x y := by
  rw [equation_iff_variableChange, nonsingular_iff_variableChange,
    equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]

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