subRight — Mathlib

English

The right n×r part of a (u+d)×n matrix is the submatrix formed by the last r columns.

Русский

Правая часть матрицы размером n×r формируется как подматрица, состоящая из последних r столбцов.

LaTeX

$$$ \text{subRight} (A) = \text{submatrix}(A, \mathrm{id}, \mathrm{natAdd}(l)) $$$

Lean4

/-- The right `n × r` part of an `n × (l+r)` matrix. -/
abbrev subRight {m l r : Nat} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin r) α :=
  submatrix A id (Fin.natAdd l)

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