flag_le_ker_coord

Mathlib.LinearAlgebra.Basis.Flag

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

← MathLib Explorer

English

If k ≤ l.castSucc then F_k ≤ ker(coord_l).

Русский

Если k ≤ l.castSucc, то F_k ⊆ ker(coord_l).

LaTeX

$$$F_k \le \ker(\mathrm{coord}_l) \text{ whenever } k \le l^{\uparrow}.$$$

Lean4

theorem flag_le_ker_coord (b : Basis (Fin n) R M) {k : Fin (n + 1)} {l : Fin n} (h : k ≤ l.castSucc) :
    b.flag k ≤ LinearMap.ker (b.coord l) := by
  nontriviality R
  exact b.flag_le_ker_coord_iff.2 h

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

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

Разделы

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

Аффилиация

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