Theorem uniformity_eq_comap_mul_inv_nhds_one_swapped

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_swappedView on Github →