Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-17 10:23
c148e3fb
View on Github →
chore: golf (
#3473
)
Golf
TopologicalGroup.toUniformSpace
.
Slightly golf
GroupSeminorm.toSeminormedGroup
Estimated changes
Modified
Mathlib/Analysis/Normed/Group/Basic.lean
modified
def
GroupSeminorm.toSeminormedGroup
Modified
Mathlib/Topology/Algebra/UniformGroup.lean
modified
def
TopologicalGroup.toUniformSpace