dualCoannihilator_top — Mathlib

English

A set of linear functionals spanning a quotient space yields finiteness of the span.

Русский

Набор линейных функционалов, порождающий фактор-пространство, обеспечивает конечность порождающего множества.

LaTeX

$$FiniteDimensional.mem_span_of_iInf_ker_le_ker$$

Lean4

@[simp]
theorem dualCoannihilator_top [Projective R M] : (⊤ : Submodule R (Module.Dual R M)).dualCoannihilator = ⊥ := by
  rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]

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