flag

Mathlib.LinearAlgebra.Basis.Flag

URI: https://scilib.ai/kg/mathlib#Module.Basis.flag

← MathLib Explorer

English

The basis of R × R obtained by the two standard basis vectors (1,0) and (0,1).

Русский

Базис пространства R × R, состоящий из двух векторов (1,0) и (0,1).

LaTeX

$$$\text{Basis}(\mathrm{Fin}~2)~\,R~(R\times R)$$$

Lean4

/-- The subspace spanned by the first `k` vectors of the basis `b`. -/
def flag (b : Basis (Fin n) R M) (k : Fin (n + 1)) : Submodule R M :=
  .span R <| b '' {i | i.castSucc < k}

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

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

Разделы

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

Аффилиация

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