toBlocks₂₁ — Mathlib

English

The right block extraction maps give the bottom-right block, etc.

Русский

Извлечение правого блока даёт нижний правый блок матрицы-результата блочно-разделения.

LaTeX

$$$\text{toBlocks}_{ij}$ for blocks$$

Lean4

/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
"bottom left" submatrix. -/
def toBlocks₂₁ (M : Matrix (n ⊕ o) (l ⊕ m) α) : Matrix o l α :=
  of fun i j => M (Sum.inr i) (Sum.inl j)

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