map_sub — Mathlib

English

Map distributes over subtraction for block matrices: (M - N).map f = M.map f - N.map f.

Русский

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

LaTeX

$$$((M - N).map f) = M.map f - N.map f$$$

Lean4

theorem map_sub [∀ i j, AddGroup (α i j)] {β : m → n → Type w} [∀ i j, AddGroup (β 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

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