English
Let A be a (u+d) × (l+r) matrix. The bottom-right block has size d × r and consists of the last d rows and last r columns; its entries satisfy ((subDownRight A))_{i j} = A_{u+i, l+j} for i = 0,…,d−1 and j = 0,…,r−1.
Русский
Пусть A — матрица размером (u+d) × (l+r). Нижний правый блок размером d × r состоит из последних d строк и последних r столбцов; его элементы удовлетворяют ((subDownRight A))_{i j} = A_{u+i, l+j} для i = 0,…,d−1 и j = 0,…,r−1.
LaTeX
$$$((\text{subDownRight } A))_{i j} = A_{u+i,\, l+j}$ for all $i \in \operatorname{Fin}(d)$, $j \in \operatorname{Fin}(r)$$$
Lean4
/-- The bottom-right `d × r` part of a `(u+d) × (l+r)` matrix. -/
abbrev subDownRight {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin r) α :=
subDown (subRight A)
