English
The matrix of a linear map respecting the direct sum decompositions has a block-diagonal form with blocks given by the restrictions to each component.
Русский
Матрица линейного отображения, сохраняющего разбиение на прямые суммы, имеет блочно-диагональный вид, элементы на диагонали — это ограничения на каждую компоненту.
LaTeX
$$toMatrix (h.collectedBasis b) (h.collectedBasis b) f = Matrix.blockDiagonal' (\i, toMatrix (b i) (b i) (f.restrict (hf i))).$$
Lean4
/-- The difference with `DirectSum.listProd_apply_eq_zero` is that the indices at which
the terms of the list are zero is allowed to vary. -/
theorem listProd_apply_eq_zero' {l : List ((⨁ i, A i) × ι)} (hl : ∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄
(hn : n < (l.map Prod.snd).sum) : (l.map Prod.fst).prod n = 0 := by
induction l generalizing n with
| nil => simp [(zero_le n).not_gt] at hn
| cons head tail
ih =>
simp only [List.mem_cons, forall_eq_or_imp, List.map_cons, List.sum_cons, List.prod_cons] at hl hn ⊢
exact mul_apply_eq_zero hl.1 (ih hl.2) hn
