English
BlockDiagonal' distributes over blockwise multiplication: blockDiagonal'(M_k · N_k) = blockDiagonal'M · blockDiagonal'N.
Русский
BlockDiagonal' распределяется по поперечному умножению блоков: blockDiagonal'(M_k N_k) = blockDiagonal'M · blockDiagonal'N.
LaTeX
$$$ \\mathrm{blockDiagonal}'(\\lambda k. M_k \\cdot N_k) = \\mathrm{blockDiagonal}' M \\cdot \\mathrm{blockDiagonal}' N $$$
Lean4
@[simp]
theorem blockDiagonal'_mul [NonUnitalNonAssocSemiring α] [∀ i, Fintype (n' i)] [Fintype o]
(M : ∀ i, Matrix (m' i) (n' i) α) (N : ∀ i, Matrix (n' i) (p' i) α) :
(blockDiagonal' fun k => M k * N k) = blockDiagonal' M * blockDiagonal' N :=
by
ext ⟨k, i⟩ ⟨k', j⟩
simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]
rw [Fintype.sum_eq_single k]
· simp only [dif_pos]
split_ifs <;> simp
· intro j' hj'
exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]