polynomialX_eq — Mathlib

English

A more detailed restatement of polynomialX above, expressed as equality of a combination of monomials in X,Y,Z with the coefficients a1,a2,a4.

Русский

Более подробное выражение polynomialX через равенство, включающее мономы X, Y, Z с коэффициентами a1, a2, a4.

LaTeX

$$$W'.polynomialX = (a_1)\\cdot Y \\cdot Z - \\bigl( 3 X^2 + 2 a_2 X Z + a_4 Z^2 \\bigr)$$$

Lean4

theorem polynomialX_eq : W'.polynomialX = C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z + C W'.a₄ * Z ^ 2) :=
  by
  rw [polynomialX, polynomial]
  pderiv_simp
  ring1

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