Theorem WithSeminorms.topologicalAddGroup

Modification history

2026-08-25 11:58
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
chore: topologicalGroup -> isTopologicalGroup in names (#43027)
Deleted WithSeminorms.topologicalAddGroupView on Github →
2025-02-16 15:19
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified WithSeminorms.topologicalAddGroupView on Github →
2023-05-24 09:57
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
feat: port Analysis.LocallyConvex.WithSeminorms (#4170)
Added WithSeminorms.topologicalAddGroupView on Github →