iInf_ker_coroot'_eq — Mathlib

English

The infimum of kernels of coroot maps equals the dual coannihilator of the span of coroot range.

Русский

Наименьшее пересечение ядер отображений корота равно двойному коаннигилятивному охвату пространства корорт'

LaTeX

$$$\bigwedge_i \ker (P.coroot' i) = (\operatorname{span}_R (\operatorname{range} P.coroot'))\.dualCoannihilator$$$

Lean4

theorem iInf_ker_coroot'_eq : ⨅ i, LinearMap.ker (P.coroot' i) = (span R (range P.coroot')).dualCoannihilator :=
  P.flip.iInf_ker_root'_eq

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