Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 07:10 30185dca

View on Github →

feat(topology/algebra/group): group topologies on a given group form a complete lattice (#10531)

Estimated changes

Modified src/topology/algebra/group.lean

added structure add_group_topology

added def group_topology.coinduced

added theorem group_topology.coinduced_continuous

added theorem group_topology.ext'

added structure group_topology

Modified src/topology/algebra/ring.lean

added def ring_topology.to_add_group_topology.order_embedding

added def ring_topology.to_add_group_topology