Theorems · Theorem · group theory
QuotientAddGroup.card_quotient_rightRel
∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst_1 : Fintype (α ⧸ s)],
Fintype.card (Quotient (QuotientAddGroup.rightRel s)) = Fintype.card (α ⧸ s)- Defined in
- Mathlib.GroupTheory.Coset.Card
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 72 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.
- Fintypestatement and proof · cited by 7,736
- AddGroupstatement and proof · cited by 4,410
- Equiv.symmproof · cited by 3,681
- AddSubgroupstatement and proof · cited by 3,232
- HasQuotient.Quotientstatement and proof · cited by 2,301
- Fintype.cardstatement · cited by 1,386
- Fintype.ofEquiv_cardproof · cited by 16
- QuotientAddGroup.rightRelstatement · cited by 14
- QuotientAddGroup.quotientRightRelEquivQuotientLeftRelproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- AddSubgroup.exists_finset_card_le_addproof · cited by 0