subDown

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.subDown

← MathLib Explorer

English

The bottom d×n part of a (u+d)×n matrix consists of the last d rows.

Русский

Нижняя часть матрицы (u+d)×n состоит из последних d строк.

LaTeX

$$$ \text{subDown} A = \text{submatrix}(A, \mathrm{natAdd}(u), \mathrm{id}) $$$

Lean4

/-- The bottom `d × n` part of a `(u+d) × n` matrix. -/
abbrev subDown {d u n : Nat} (A : Matrix (Fin (u + d)) (Fin n) α) : Matrix (Fin d) (Fin n) α :=
  submatrix A (Fin.natAdd u) id

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru