negDblY_smul — Mathlib

English

The Y-coordinate negDblY scales homogeneously under scalar multiplication: negDblY(u·P) = (u^4)^3 · negDblY(P).

Русский

Y-координата negDblY многочленно гомогенно по отношению к умножению на скаляр: negDblY(u·P) = (u^4)^3 · negDblY(P).

LaTeX

$$$W'.\\mathrm{negDblY}(u \\cdot P) = (u^4)^3 \\cdot W'.\\mathrm{negDblY}(P)$$$

Lean4

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

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