Theorem IsCompact.mul

Modification history

2026-02-26 16:02

Mathlib/Topology/Algebra/Monoid.lean

feat: `SeparatelyContinuousMul` class for multiplication which is continuous in each variable (#35589) …

Modified IsCompact.mul View on Github →

2023-02-14 14:45

Mathlib/Topology/Algebra/Monoid.lean

feat: port Topology.Algebra.Monoid (#2245)

Added IsCompact.mul View on Github →