monoid): changed topological_monoid into has_continuous_mul (#3481)

Commit

5 years ago

refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481) Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Author

Nicknamen

Parents

079d4093

mathlib 0322d892 - refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481)

mathlib
0322d892 - refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481)