map_add — Mathlib

English

If f preserves addition, then mapping distributes over matrix addition: (M+N).map f = M.map f + N.map f.

Русский

Если f сохраняет сложение, отображение распределено по сложению матриц: (M+N).map f = M.map f + N.map f.

LaTeX

$$$ (M + N).map\\ f = M.map\\ f + N.map\\ f $$$

Lean4

protected theorem map_add [Add α] [Add β] (f : α → β) (hf : ∀ a₁ a₂, f (a₁ + a₂) = f a₁ + f a₂) (M N : Matrix m n α) :
    (M + N).map f = M.map f + N.map f :=
  ext fun _ _ => hf _ _

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