English
Let BM be an AddGroupFilterBasis on M and BR a RingFilterBasis on R; using compatible smul data, one can form a ModuleFilterBasis; its topology on M is induced by its AddGroupFilterBasis topology.
Русский
Пусть BM — AddGroupFilterBasis на M и BR — RingFilterBasis на R; используя совместимые данные умножения, можно образовать ModuleFilterBasis; его топология на M задаётся через topology AddGroupFilterBasis.
LaTeX
$$$\text{ModuleFilterBasis.topology}(R,M,BM,BR) : \text{TopologicalSpace } M$.$$
Lean4
/-- The topology associated to a module filter basis on a module over a topological ring.
It has the given basis as a basis of neighborhoods of zero. -/
def topology : TopologicalSpace M :=
B.toAddGroupFilterBasis.topology
