Commit 2023-12-05 05:47 9ea21ba0

View on Github →

feat(UniformGroup): add UniformInducing.uniformGroup (#8813)

Estimated changes

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

Modified Mathlib/Topology/Algebra/UniformGroup.lean

added theorem UniformInducing.uniformGroup

deleted theorem uniformGroup_comap