Revision #1631 → #2663 · back to history
modifiedReal numbers and Euclidean space as topological groupsc58eb5c70ead
| Field | From #1631 | To #2663 |
|---|
| mathlib.decl | Real.instIsTopologicalAddGroup | instIsTopologicalAddGroupReal |
| provenance | ai | ai-moderated |
modifiedInvertible elements of Banach algebra83ce5708a47a
| Field | From #1631 | To #2663 |
|---|
| mathlib.decl | Units.instIsTopologicalGroup | Units.instIsTopologicalGroupOfContinuousMul |
| provenance | ai | ai-moderated |
modifiedSubgroup is a topological group982fdac0b3b6
| Field | From #1631 | To #2663 |
|---|
| mathlib.decl | Subgroup.instIsTopologicalGroup | Subgroup.instIsTopologicalGroupSubtypeMem |
| provenance | ai | ai-moderated |
modifiedSequentially complete topological groupc763029cdb4a
| Field | From #1631 | To #2663 |
|---|
| mathlib.decl | SequentiallyComplete | UniformSpace.complete_of_cauchySeq_tendsto |
| provenance | ai | ai-moderated |