blockDiag'_map — Mathlib

English

With DecidableEq on each m'_i, addition distributes: blockDiagonal'(M + N) = blockDiagonal' M + blockDiagonal' N.

Русский

При заданииDecidableEq на каждом m'_i сложение распределяется: blockDiagonal'(M+N) = blockDiagonal' M + blockDiagonal' N.

LaTeX

$$$ \\mathrm{blockDiagonal}'(M + N) = \\mathrm{blockDiagonal}' M + \\mathrm{blockDiagonal}' N $$$

Lean4

theorem blockDiag'_map (M : Matrix (Σ i, m' i) (Σ i, n' i) α) (f : α → β) :
    blockDiag' (M.map f) = fun k => (blockDiag' M k).map f :=
  rfl

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