blockDiagonal'_submatrix_eq_blockDiagonal

English

The value of blockDiagonal' M at indices ⟨k,i⟩, ⟨k',j⟩ is given by a conditional: M k i j if k = k' and 0 otherwise.

Русский

Значение blockDiagonal' M в ⟨k,i⟩, ⟨k',j⟩ равно M_k i j при k = k' и 0 при иначе.

LaTeX

$$$ blockDiagonal' M \langle k,i\rangle \langle k',j\rangle = \begin{cases} M k i j, & \text{если } k = k' \\ 0, & \text{иначе} \end{cases} $$$

Lean4

theorem blockDiagonal'_submatrix_eq_blockDiagonal (M : o → Matrix m n α) :
    (blockDiagonal' M).submatrix (Prod.toSigma ∘ Prod.swap) (Prod.toSigma ∘ Prod.swap) = blockDiagonal M :=
  Matrix.ext fun ⟨_, _⟩ ⟨_, _⟩ => rfl

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