flag_le_ker_dual — Mathlib

English

For a basis b, the flag at k is contained in the kernel of the dual basis map: F_k ≤ ker(b.dualBasis_k).

Русский

Для базиса b флаг в позиции k содержится в ядре двойственного отображения: F_k ⊆ ker(dualBasis_k).

LaTeX

$$$F_k \le \ker(b.dualBasis_k)$$$

Lean4

theorem flag_le_ker_dual (b : Basis (Fin n) R M) (k : Fin n) : b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k) :=
  by
  nontriviality R
  rw [coe_dualBasis, b.flag_le_ker_coord_iff]

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