equation_iff' — Mathlib

English

The equation is equivalent to a specific polynomial equality: W.Equation x y holds iff a quadratic identity in x,y vanishes.

Русский

Уравнение эквивалентно равенству полиномов: W.Equation x y эквивалентно нулю для выражения в x,y.

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₆) = 0$$

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₆) = 0 := by
  rw [Equation, evalEval_polynomial]

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