map_smulₛₗ — Mathlib

English

With a morphism σ: R → S and r ∈ R, (r • M).map f = σ(r) • M.map f, whenever f respects the corresponding scalar action.

Русский

С учётом отображения σ: R → S и элемента r ∈ R, (r • M).map f = σ(r) • M.map f при условии, что f сохраняет соответствующее скалярное действие.

LaTeX

$$$ (r \\cdot M).map\\ f = (\\sigma r) \\cdot (M.map\\ f) $$$

Lean4

protected theorem map_smulₛₗ [SMul R α] [SMul S β] (f : α → β) (σ : R → S) (r : R) (hf : ∀ a, f (r • a) = σ r • f a)
    (M : Matrix m n α) : (r • M).map f = σ r • M.map f :=
  ext fun _ _ => hf _

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