smul_fin3 — Mathlib

English

There is a natural coordinatewise scalar action on the Fin 3 → R: for all u ∈ R and P ∈ Fin 3 → R, u • P is defined by applying the scalar on each coordinate with appropriate powers, yielding a coherent MulAction.

Русский

Существует естественное по координатам скалярное действие на Fin 3 → R: для каждого u ∈ R и P ∈ Fin 3 → R определено u • P, действующее по координатам с соответствующими степенями так, чтобы образовалось согласованное действие MulAction.

LaTeX

$$$\text{MulAction}$ на $(\text{Fin }3 \to R)$ действующее по координатам$$

Lean4

theorem smul_fin3 (P : Fin 3 → R) (u : R) : u • P = ![u ^ 2 * P x, u ^ 3 * P y, u * P z] :=
  rfl

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