negDblY_smul — Mathlib

English

A variant of negDblY_eq' expressing negDblY P in terms of a cubic power of P 2 and a negation divided by W'.polynomialX.

Русский

Вариант negDblY_eq', выражающий negDblY P через кубический степенной член (P 2)^3 и деление на W'.polynomialX.

LaTeX

$$$ {P: Fin 3 → F} (hP: W'.Equation P) : W'.negDblY P \cdot P z^2 = - eval P W'.polynomialX^3$$$

Lean4

theorem negDblY_smul (P : Fin 3 → R) (u : R) : W'.negDblY (u • P) = u ^ 4 * W'.negDblY P :=
  by
  simp only [negDblY, smul_fin3_ext]
  ring1

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