blockDiagonal'_mul — Mathlib

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]

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