Theorem ContinuousMul.induced

Modification history

2025-04-09 00:36

Mathlib/Topology/Algebra/Monoid.lean

feat: generalize Mathlib.Topology (#23193) …

Modified ContinuousMul.induced View on Github →

2024-07-21 01:25

Mathlib/Topology/Algebra/Monoid.lean

feat: define the weak operator topology (#14177) …

Added ContinuousMul.induced View on Github →