Theorems · Inductive type · Lie groups
OpenNormalAddSubgroup
(G : Type u) → [AddGroup G] → [TopologicalSpace G] → Type u
The type of open normal subgroups of a topological additive group.
- Defined in
- Mathlib.Topology.Algebra.OpenSubgroup
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddGroupTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- AddGroupstatement · cited by 4,410
Cited by37
Results whose statement or proof uses this declaration.
- ProfiniteAddGrp.diagramstatement · cited by 6
- OpenNormalAddSubgroup.toOpenAddSubgroupstatement and proof · cited by 6
- OpenNormalAddSubgroup.extstatement and proof · cited by 2
- ProfiniteAddGrp.toFiniteQuotientFunctorstatement and proof · cited by 2
- OpenNormalAddSubgroup.toFiniteIndexNormalAddSubgroupstatement and proof · cited by 2
- ProfiniteGrp.exist_openNormalAddSubgroup_sub_open_nhds_of_zerostatement and proof · cited by 2
- ProfiniteAddGrp.conestatement · cited by 2
- IsTopologicalAddGroup.exist_openNormalAddSubgroup_sub_clopen_nhds_of_zerostatement · cited by 1
- ProfiniteAddGrp.ProfiniteCompletion.preimagestatement and proof · cited by 1
- ProfiniteAddGrp.projstatement and proof · cited by 1
- OpenNormalAddSubgroup.mk.injstatement · cited by 1
- ProfiniteAddGrp.toLimitstatement · cited by 1