iInf_ker_root'_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_ker_root'_eq : ⨅ i, LinearMap.ker (P.root' i) = (span R (range P.root')).dualCoannihilator := by
  rw [← rootSpan_dualAnnihilator_map_eq, rootSpan_dualAnnihilator_map_eq_iInf_ker_root']

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