Theorems · Definition · group theory

AddSubgroup.IsComplement.rightQuotientEquiv

{G : Type u_1} →
  [inst : AddGroup G] →
    {H : AddSubgroup G} → {T : Set G} → AddSubgroup.IsComplement (↑H) T → Quotient (QuotientAddGroup.rightRel H) ≃ ↑T

A right transversal is in bijection with right cosets.

Defined in: Mathlib.GroupTheory.Complement
Cited by: 5 results in Mathlib
Foundations: Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

Setstatement and proof · cited by 53,352
Equivstatement · cited by 8,337
SetLike.coestatement and proof · cited by 8,199
Set.Elemstatement · cited by 7,166
AddGroupstatement and proof · cited by 4,410
Equiv.symmproof · cited by 3,681
AddSubgroupstatement and proof · cited by 3,232
Set.domRestrictproof · cited by 383
Quotient.mk''proof · cited by 132
Equiv.ofBijectiveproof · cited by 70
AddSubgroup.IsComplementstatement and proof · cited by 57
QuotientAddGroup.rightRelstatement · cited by 14

Cited by6

Results whose statement or proof uses this declaration.

AddSubgroup.IsComplement.toRightFunproof · cited by 7
AddSubgroup.IsComplement.finite_right_iffproof · cited by 1
AddSubgroup.IsComplement.mk''_rightQuotientEquivstatement and proof · cited by 1
ProperlyDiscontinuousVAdd.ofFiniteRelIndexproof · cited by 1
AddSubgroup.IsComplement.rightQuotientEquiv_applystatement and proof · cited by 0
AddSubgroup.exists_finset_card_le_addproof · cited by 0