smul_fin3 — Mathlib

English

For any P: Fin 3 → R and u ∈ R, the scalar product is coordinatewise: u • P = ![u · P x, u · P y, u · P z].

Русский

Для любого P: Fin 3 → R и u ∈ R скалярное умножение действует по координатам: u • P = ![u·P x, u·P y, u·P z].

LaTeX

$$$u \cdot P = ![u \cdot P x, u \cdot P y, u \cdot P z]$$$

Lean4

theorem smul_fin3 (P : Fin 3 → R) (u : R) : u • P = ![u * P x, u * P y, u * P z] := by
  simp [← List.ofFn_inj, List.ofFn_succ]

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