Commit 2020-09-21 18:45 b91df551

View on Github →

chore(topology/algebra/module): make topological_module an abbreviation (#4200) Also prove that a topological_semiring is a topological_semimodule.

Estimated changes

Modified src/topology/algebra/module.lean

added def topological_module