equation_iff — Mathlib

English

Expanding the equation and reorganizing terms yields an explicit cubic condition.

Русский

Раскрывшееся однородное уравнение W'(X, Y, Z) = 0 даёт явное кубическое уравнение в X, Y, Z: Y^2 Z + a1 X Y Z + a3 Y Z^2 − (X^3 + a2 X^2 Z + a4 X Z^2 + a6 Z^3) = 0.

LaTeX

$$$W'.Equation(P) \\iff P y^{2} P z + W'.a_{1} P x P y P z + W'.a_{3} P y P z^{2} - (P x^{3} + W'.a_{2} P x^{2} P z + W'.a_{4} P x P z^{2} + W'.a_{6} P z^{3}) = 0$$$

Lean4

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

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