Mathlib Map

Theorems · Inductive type · group theory

Subgroup.FiniteIndex

{G : Type u_1} → [inst : Group G] → Subgroup G → Prop

Typeclass for finite index subgroups.

Defined in
Mathlib.GroupTheory.Index
Cited by
113 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Rep.indCoindIso · cited by 13Rep.indCoindIsoSubgroup.FiniteIndex.index_ne_zero · cited by 12FiniteIndex.index_ne_zeroMonoidHom.transferSylow · cited by 9MonoidHom.transferSylowSylow.not_dvd_index · cited by 9Sylow.not_dvd_indexSubgroup.fintypeQuotientOfFiniteIndex · cited by 9Subgroup.fintypeQuotientO…Subgroup.leftTransversals.diff · cited by 8leftTransversals.diffMonoidHom.transfer · cited by 6MonoidHom.transferRep.coindToInd · cited by 6Rep.coindToIndRep.indCoindNatIso · cited by 6Rep.indCoindNatIsoSubgroup.finiteIndex_of_finite_quotient · cited by 6Subgroup.finiteIndex_of_f…Subgroup.transferFocal · cited by 5Subgroup.transferFocalSubgroup.finiteIndex_iff · cited by 5Subgroup.finiteIndex_iffRep.coindResAdjunction · cited by 4Rep.coindResAdjunctionRep.resIndAdjunction · cited by 4Rep.resIndAdjunctionSubgroup.QuotientDiff · cited by 3Subgroup.QuotientDiffGroup · cited by 6238GroupSubgroup · cited by 3593SubgroupSubgroup.FiniteIndexCITED BYCITES

Cites2

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

  • Groupstatement · cited by 6,238
  • Subgroupstatement · cited by 3,593

Cited by135

Results whose statement or proof uses this declaration.