English
A similar statement as above for a different basis configuration shows the same block-diagonal decomposition of the matrix.
Русский
Та же идея для другой конфигурации базисов дает блочно-диагональное разложение матрицы.
LaTeX
$$toMatrix (h.collectedBasis b) (h.collectedBasis b) f = Matrix.blockDiagonal' (\i, toMatrix (b i) (b i) (f.restrict (hf i))).$$
Lean4
theorem listProd_apply_eq_zero {l : List (⨁ i, A i)} {m : ι} (hl : ∀ x ∈ l, ∀ k < m, x k = 0) ⦃n : ι⦄
(hn : n < l.length • m) : l.prod n = 0 := by
-- a proof which uses `DirectSum.listProd_apply_eq_zero'` is actually more work
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.length_cons, List.prod_cons] at hl hn ⊢
refine mul_apply_eq_zero hl.1 (ih hl.2) ?_
simpa [add_smul, add_comm m] using hn
