moduleFilterBasis

Mathlib.Topology.Algebra.Nonarchimedean.Bases

URI: https://scilib.ai/kg/mathlib#RingFilterBasis.moduleFilterBasis

Lean4

/-- The module filter basis associated to a ring filter basis and a compatible submodule basis.
This allows to build a topological module structure compatible with the given module structure
and the topology associated to the given ring filter basis. -/
def moduleFilterBasis [Nonempty ι] (BR : RingFilterBasis R) {B : ι → Submodule R M} (hB : BR.SubmodulesBasis B) :
    @ModuleFilterBasis R M _ BR.topology _ _ :=
  @SubmodulesBasis.toModuleFilterBasis ι R _ M _ _ BR.topology _ _ (BR.submodulesBasisIsBasis hB)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru