equation_iff — Mathlib

English

The equation form is equivalent to the standard polynomial equality expressed above.

Русский

Уравнение эквивалентно стандартному равенству полинома, указанному выше.

LaTeX

$$W.Equation x y ↔ y^2 + W.a₁ x y + W.a₃ y = x^3 + W.a₂ x^2 + W.a₄ x + W.a₆$$

Lean4

theorem equation_iff (x y : R) :
    W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆ := by
  rw [equation_iff', sub_eq_zero]

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