Revision #3248 → #4082 · back to history
addedTopological groups as group objectsc629d1b32f7d
modifiedReal numbers and Euclidean space as topological groupsc58eb5c70ead
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.Instances.Real | Mathlib.Topology.Algebra.Ring.Real |
addedCircle group and torus7d9a06f2303f
modifiedGeneral linear group12270310b0cf
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Group.Matrix | Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs |
modifiedInvertible elements of Banach algebra83ce5708a47a
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Group.Units | Mathlib.Topology.Algebra.Group.Basic |
modifiedHausdorff quotient by closure of identityb82f74c339d5
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.SeparationQuotient.Basic | Mathlib.Topology.Defs.Filter |
modifiedMetrisable topological group12c5d9997d65
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.MetricSpace.Metrizable | Mathlib.Topology.Metrizable.Basic |
addedℝ/ℤ isomorphic to circle group34d5a9ec1f08
addedQuotient by identity component is totally disconnectedaa5a8f5b56b2
addedThird isomorphism theorem for topological groupse2c2c167d60a
modifiedTotally disconnected locally compact group contains compact open subgroup06414c2b0e40
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected | Mathlib.Topology.Connected.TotallyDisconnected |
addedHaar measure0064a502ec53
addedLocally compact commutative groups are completef5f85d33549f
modifiedUniform continuity between topological groupsbbbc848e91e6
| Field | From #3248 | To #4082 |
|---|
| mathlib.module | Mathlib.Topology.UniformSpace.UniformContinuous | Mathlib.Topology.UniformSpace.Defs |