Theorems · Theorem · group theory
AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zero
∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {X : Type u_3} [inst_1 : AddAction G X]
[Finite (AddAction.orbitRel.Quotient G X)], H.index ≠ 0 → Finite (AddAction.orbitRel.Quotient (↥H) X)- Defined in
- Mathlib.GroupTheory.Index
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypeproof · cited by 7,736
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- Finitestatement and proof · cited by 3,029
- HasQuotient.Quotientproof · cited by 2,301
- AddActionstatement and proof · cited by 820
- AddSubgroup.indexstatement and proof · cited by 104
- AddAction.orbitRel.Quotientstatement and proof · cited by 17
- AddSubgroup.fintypeOfIndexNeZeroproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zeroproof · cited by 0