Theorem uniformity_eq_comap_mul_inv_nhds_one

Modification history

2025-11-06 11:18

Mathlib/Topology/Algebra/IsUniformGroup/Defs.lean

feat: define IsRightUniformGroup and IsLeftUniformGroup (#30029) …

Added uniformity_eq_comap_mul_inv_nhds_one View on Github →