Subgroup.isComplement_subgroup_left_iff_bijective

∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G},
  Subgroup.IsComplement (↑H) T ↔ Function.Bijective (T.domRestrict Quotient.mk'')

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

Around this declaration

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

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
SetLike.coestatement · cited by 8,199
Set.Elemstatement · cited by 7,166
Groupstatement and proof · cited by 6,238
Subgroupstatement and proof · cited by 3,593
Function.Bijectivestatement · cited by 863
Set.domRestrictstatement and proof · cited by 383
Quotient.mk''statement and proof · cited by 132
Subgroup.IsComplementstatement · cited by 94
QuotientGroup.rightRelstatement · cited by 44
Function.bijective_iff_existsUniqueproof · cited by 15
Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk''proof · cited by 1

Results whose statement or proof uses this declaration.