addZ_smul — Mathlib

English

The additive coordinate map respects scalar multiplication in a bilinear way: addZ(u·P, v·Q) = (uv)^2 · addZ(P,Q).

Русский

Координаты сложения уравновешивают скалярное умножение: addZ(u·P, v·Q) = (uv)^2 · addZ(P,Q).

LaTeX

$$$W'.addZ(u\cdot P, v\cdot Q) = (u v)^2 \cdot W'.addZ(P,Q)$$$

Lean4

theorem addZ_smul (P Q : Fin 3 → R) (u v : R) : W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q :=
  by
  simp only [addZ, smul_fin3_ext]
  ring1

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