smul_fin3_ext — Mathlib

English

For the Fin 3-vector P and scalar u, the action is given coordinatewise: (u • P)_0 = u^2 P_0, (u • P)_1 = u^3 P_1, (u • P)_2 = u P_2.

Русский

Для вектора Fin 3 → R и скаляра u действие выполняется по координатам: (u • P)_0 = u^2 P_0, (u • P)_1 = u^3 P_1, (u • P)_2 = u P_2.

LaTeX

$$$(u \cdot P)_x = u^2 P_x \land (u \cdot P)_y = u^3 P_y \land (u \cdot P)_z = u P_z$$

Lean4

theorem smul_fin3_ext (P : Fin 3 → R) (u : R) :
    (u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z :=
  ⟨rfl, rfl, rfl⟩

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