dualCoannihilator_bot — Mathlib

English

Let R be a commutative semiring and M an R-module. The dual coannihilator of the zero submodule of the dual of M is the whole dual space, i.e., the dual coannihilator of ⊥ in Module.Dual(R,M) equals ⊤.

Русский

Пусть R — коммутативная полускольная кольцо, M — модуль над R. Дуальный коаннигилятор нуля подмодуля в пространстве двойственных функционалов равен всему пространству (⊤).

LaTeX

$$$ (\\bot : \\mathrm{Submodule} \\, R \\, (\\mathrm{Module.Dual} \\, R \\, M)).\\mathrm{dualCoannihilator} = \\top $$$

Lean4

@[simp]
theorem dualCoannihilator_bot : (⊥ : Submodule R (Module.Dual R M)).dualCoannihilator = ⊤ :=
  (dualAnnihilator_gc R M).u_top

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