blockDiagonal'_apply' — Mathlib

English

The blockDiagonal M and blockDiagonal' M agree on corresponding entries: blockDiagonal M (i, k) (j, k') equals blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩.

Русский

Для любых индексов блок-матриц совпадают значения: blockDiagonal M (i,k) (j,k') = blockDiagonal' M ⟨k,i⟩ ⟨k',j⟩.

LaTeX

$$$ blockDiagonal M (i,k) (j,k') = blockDiagonal' M \langle k,i \rangle \langle k', j \rangle $$$

Lean4

theorem blockDiagonal'_apply' (M : ∀ i, Matrix (m' i) (n' i) α) (k i k' j) :
    blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ = if h : k = k' then M k i (cast (congr_arg n' h.symm) j) else 0 :=
  rfl

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