toRows₂ — Mathlib

English

From a row-partitioned matrix A of size (m1 ⊕ m2) × n, extract the second row block as a matrix of size m2 × n by taking entries A(Sum.inr i, j).

Русский

Из матрицы A размера (m1 ⊕ m2) × n извлекаем второй блок строк размером m2 × n, взяв элементы A(Sum.inr i, j).

LaTeX

$$$\\text{toRows₂}(A)_{i j} = A_{(Sum.inr i),\,j}$$$

Lean4

/-- Given a row partitioned matrix extract the second row -/
def toRows₂ (A : Matrix (m₁ ⊕ m₂) n R) : Matrix m₂ n R :=
  of fun i j => (A (Sum.inr i) j)

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