English
The sum of blockDiagonal' equals the blockDiagonal' of tsum.
Русский
Сумма по blockDiagonal' равна blockDiagonal'(сумме).
LaTeX
$$blockDiagonal' (tsum(f,L)) = tsum(λ x, blockDiagonal'(f x), L)$$
Lean4
theorem blockDiagonal'_tsum [DecidableEq l] [T2Space R] {f : X → ∀ i, Matrix (m' i) (n' i) R} :
blockDiagonal' (∑'[L] x, f x) = ∑'[L] x, blockDiagonal' (f x) :=
Function.LeftInverse.map_tsum (g := blockDiagonal'AddMonoidHom m' n' R) f continuous_id.matrix_blockDiagonal'
continuous_id.matrix_blockDiag' blockDiag'_blockDiagonal'