map_add — Mathlib

English

Map distributes over addition for block matrices: map f distributes across (M+N).

Русский

Отображение DMatrix по сумме распределяет сумму: (M+N).map f = M.map f + N.map f.

LaTeX

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

Lean4

theorem map_add [∀ i j, AddMonoid (α i j)] {β : m → n → Type w} [∀ i j, AddMonoid (β i j)] (f : ∀ ⦃i j⦄, α i j →+ β i j)
    (M N : DMatrix m n α) : ((M + N).map fun i j => @f i j) = (M.map fun i j => @f i j) + N.map fun i j => @f i j := by
  ext; simp

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