Commit 2023-08-31 09:57 65823582

View on Github →

chore(Topology/Algebra/Group): golf, move (#6820) Move some lemmas from Topology.Algebra.UniformGroup to Topology.Algebra.Group.Basic, golf.

Estimated changes

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem TopologicalGroup.t2Space_iff_one_closed

added theorem TopologicalGroup.t2Space_of_one_sep

Modified Mathlib/Topology/Algebra/UniformGroup.lean

deleted theorem TopologicalGroup.t2Space_iff_one_closed

deleted theorem TopologicalGroup.t2Space_of_one_sep