addU_smul — Mathlib

English

For scalars u,v and projective inputs P,Q, the value of addU scales as addU(u·P, v·Q) = (uv)^2 · addU(P,Q).

Русский

При масштабировании входов на скаляры u и v, значение addU масштабируется как addU(u·P, v·Q) = (uv)^2 · addU(P,Q).

LaTeX

$$$\forall P,Q:\ Fin(3) \to F,\forall u,v:\ F,\ addU(u\cdot P, v\cdot Q) = (u v)^2 \cdot addU(P,Q)$$$

Lean4

theorem addU_smul (P Q : Fin 3 → F) (u v : F) : addU (u • P) (v • Q) = (u * v) ^ 2 * addU P Q := by simp [field, addU]

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