Theorems · Inductive type · group theory
Subgroup.IsFiniteRelIndex
{G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G → PropTypeclass for a subgroup H to have finite index in a subgroup K.
- Defined in
- Mathlib.GroupTheory.Index
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Group
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.
Cited by33
Results whose statement or proof uses this declaration.
- Subgroup.relIndex_ne_zerostatement and proof · cited by 5
- ModularForm.normstatement and proof · cited by 5
- Subgroup.isFiniteRelIndex_iff_relIndex_ne_zerostatement and proof · cited by 3
- ModularForm.tracestatement and proof · cited by 2
- Subgroup.isFiniteRelIndex_iff_finiteIndexstatement · cited by 2
- SlashInvariantForm.normstatement and proof · cited by 2
- ModularForm.coe_normstatement and proof · cited by 2
- IsCusp.of_isFiniteRelIndexstatement and proof · cited by 1
- Subgroup.discreteTopology_iff_of_isFiniteRelIndexstatement and proof · cited by 1
- ProperlyDiscontinuousSMul.ofFiniteRelIndexstatement and proof · cited by 1
- Subgroup.isFiniteRelIndex_of_le_leftstatement and proof · cited by 1
- Subgroup.isFiniteRelIndex_of_le_rightstatement and proof · cited by 1