addZ_smul — Mathlib

English

For P,Q in Fin3 → R and scalars u,v in R, the Z-coordinate scales quadratically with the product of the scalars: addZ(u·P, v·Q) = (uv)^2 · addZ(P,Q).

Русский

Для P,Q ∈ (Fin 3 → R) и скаляров u,v ∈ R Z-координата при суммировании масштабированных точек масштабируется квадратно: addZ(u·P, v·Q) = (uv)^2 · addZ(P,Q).

LaTeX

$$$\operatorname{addZ}(u\cdot P, v\cdot Q) = (uv)^2 \cdot \operatorname{addZ}(P,Q)$$$

Lean4

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

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