All.lean
Nyll.ProCGroups.Topologies.All
0 declarations indexed from sourceView source ↗
Module documentation
Topological-group infrastructure
This aggregate module exposes continuous homomorphisms and equivalences, conjugation, open and characteristic subgroups, quotient maps, and full subgroup topologies.
Imports7
- Nyll.ProCGroups.Topologies.Conjugation
- Nyll.ProCGroups.Topologies.ContinuousMonoidHom
- Nyll.ProCGroups.Topologies.ContinuousMulEquiv
- Nyll.ProCGroups.Topologies.FullSubgroupTopology.All
- Nyll.ProCGroups.Topologies.OpenSubgroup
- Nyll.ProCGroups.Topologies.QuotientMaps
- Nyll.ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
Imported by1
This module has no indexed declarations. Its imports and full source are available here.