polynomialY_eq — Mathlib

English

If P z = 0, then from the projective equation it follows that P x^3 = 0 whenever W'.Equation P holds (in a NoZeroDivisors setting).

Русский

Если P z = 0, то из проективного уравнения следует, что при условии W'.Equation P выполняется P x^3 = 0 (при отсутствии нетривиальных делителей).

LaTeX

$$$W'.Equation P \\land P z = 0 \\Rightarrow P x^{3} = 0$$$

Lean4

theorem polynomialY_eq : W'.polynomialY = C 2 * Y * Z + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 2 :=
  by
  rw [polynomialY, polynomial]
  pderiv_simp
  ring1

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