annihilator_span — Mathlib

English

The annihilator of a span equals the infimum over all generators of the span of the corresponding kernels.

Русский

Аннигилятор охвата равен инфимууму по всем порождающим охванам его ядер.

LaTeX

$$$ (\\operatorname{span}_R(s)).annihilator = \\bigwedge_{g \\in s} \\ker(\\operatorname{toSpanSingleton}_R^M(g)). $$$

Lean4

theorem annihilator_span (s : Set M) : (Submodule.span R s).annihilator = ⨅ g : s, ker (toSpanSingleton R M g.1) := by
  ext; simp [mem_annihilator_span]

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