Theorem IsTopologicalRing.to_topologicalAddGroup

Modification history

2026-08-25 11:58
Mathlib/Topology/Algebra/Ring/Basic.lean
chore: topologicalGroup -> isTopologicalGroup in names (#43027)
Deleted IsTopologicalRing.to_topologicalAddGroupView on Github →
2026-03-26 18:37
Mathlib/Topology/Algebra/Ring/Basic.lean
feat: add `IsSemitopologicalRing` (#36617) …
Added IsTopologicalRing.to_topologicalAddGroupView on Github →