Theorems · Definition · group theory
AddSubgroup.addGroupEquivQuotientProdAddSubgroup
{α : Type u_1} → [inst : AddGroup α] → {s : AddSubgroup α} → α ≃ (α ⧸ s) × ↥sA (non-canonical) bijection between an AddGroup α and the product (α/s) × s
- Defined in
- Mathlib.GroupTheory.Coset.Basic
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- 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
- QuotientAddGroup.mkproof · cited by 348
- Equiv.reflproof · cited by 274
- Quotient.outproof · cited by 141
- Quotient.mk''proof · cited by 132
- Equiv.sigmaEquivProdproof · cited by 47
- Equiv.sigmaFiberEquivproof · cited by 18
- Equiv.sigmaCongrRightproof · cited by 12
Cited by7
Results whose statement or proof uses this declaration.
- addOrderOf_dvd_cardproof · cited by 5
- finite_iff_addSubgroup_quotientproof · cited by 2
- AddSubgroup.card_eq_card_quotient_mul_card_addSubgroupproof · cited by 2
- Submodule.card_eq_card_quotient_mul_cardproof · cited by 1
- AddAction.orbitProdStabilizerEquivAddGroupproof · cited by 1
- AddAction.card_eq_sum_card_addGroup_sub_card_stabilizer'proof · cited by 1
- AddGroup.fintypeOfKerLeRangeproof · cited by 0