Mathlib Map

Theorems · Inductive type · group theory

FiniteIndexNormalSubgroup

(G : Type u_1) → [Group G] → Type u_1

The type of finite-index normal subgroups of a group.

Defined in
Mathlib.GroupTheory.FiniteIndexNormalSubgroup
Cited by
27 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FiniteIndexNormalSubgroup.toSubgroup · cited by 15FiniteIndexNormalSubgroup…FiniteIndexNormalSubgroup.comap · cited by 4FiniteIndexNormalSubgroup…Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup · cited by 3Group.residuallyFinite_if…ProfiniteGrp.ProfiniteCompletion.etaFn · cited by 2ProfiniteCompletion.etaFnProfiniteGrp.ProfiniteCompletion.diagram · cited by 2ProfiniteCompletion.diagr…FiniteIndexNormalSubgroup.ext · cited by 2FiniteIndexNormalSubgroup…ProfiniteGrp.ProfiniteCompletion.preimage · cited by 2ProfiniteCompletion.preim…FiniteIndexNormalSubgroup.ofSubgroup · cited by 2FiniteIndexNormalSubgroup…OpenNormalSubgroup.toFiniteIndexNormalSubgroup · cited by 2OpenNormalSubgroup.toFini…Group.ResiduallyFinite.iInf_eq_bot · cited by 1ResiduallyFinite.iInf_eq_…FiniteIndexNormalSubgroup.mk.inj · cited by 1mk.injFiniteIndexNormalSubgroup.mk.noConfusion · cited by 1mk.noConfusionProfiniteGrp.ProfiniteCompletion.denseRange · cited by 1ProfiniteCompletion.dense…FiniteIndexNormalSubgroup.comap_mono · cited by 1FiniteIndexNormalSubgroup…ProfiniteGrp.ProfiniteCompletion.lift_eta · cited by 1ProfiniteCompletion.lift_…Group · cited by 6238GroupFiniteIndexNormalSubgroupCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Groupstatement · cited by 6,238

Cited by43

Results whose statement or proof uses this declaration.