Cosets

This file develops the basic theory of left and right cosets.

Main definitions

• leftCoset a s: the left coset a * s for an element a : α and a subset s ⊆ α, for an AddGroup this is leftAddCoset a s.
• rightCoset s a: the right coset s * a for an element a : α and a subset s ⊆ α, for an AddGroup this is rightAddCoset s a.
• QuotientGroup.quotient s: the quotient type representing the left cosets with respect to a subgroup s, for an AddGroup this is QuotientAddGroup.quotient s.
• QuotientGroup.mk: the canonical map from α to α/s for a subgroup s of α, for an AddGroup this is QuotientAddGroup.mk.
• Subgroup.leftCosetEquivSubgroup: the natural bijection between a left coset and the subgroup, for an AddGroup this is AddSubgroup.leftCosetEquivAddSubgroup.

Notation

• a *l s: for leftCoset a s.

• a +l s: for leftAddCoset a s.

• s *r a: for rightCoset s a.

• s +r a: for rightAddCoset s a.

• G ⧸ H is the quotient of the (additive) group G by the (additive) subgroup H

def leftAddCoset {α : Type u_1} [Add α] (a : α) (s : Set α) : Set α

The left coset a+s for an element a : α and a subset s : set α

def leftCoset {α : Type u_1} [Mul α] (a : α) (s : Set α) : Set α

The left coset a * s for an element a : α and a subset s : Set α

def rightAddCoset {α : Type u_1} [Add α] (s : Set α) (a : α) : Set α

The right coset s+a for an element a : α and a subset s : set α

def rightCoset {α : Type u_1} [Mul α] (s : Set α) (a : α) : Set α

The right coset s * a for an element a : α and a subset s : Set α

def Coset.«term_*l_» : Lean.TrailingParserDescr

The left coset a * s for an element a : α and a subset s : Set α

def Coset.«term_+l_» : Lean.TrailingParserDescr

The left coset a+s for an element a : α and a subset s : set α

def Coset.«term_*r_» : Lean.TrailingParserDescr

The right coset s * a for an element a : α and a subset s : Set α

def Coset.«term_+r_» : Lean.TrailingParserDescr

The right coset s+a for an element a : α and a subset s : set α

theorem mem_leftAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : a + x ∈ leftAddCoset a s

theorem mem_leftCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : a * x ∈ leftCoset a s

theorem mem_rightAddCoset {α : Type u_1} [Add α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : x + a ∈ rightAddCoset s a

theorem mem_rightCoset {α : Type u_1} [Mul α] {s : Set α} {x : α} (a : α) (hxS : x ∈ s) : x * a ∈ rightCoset s a

def LeftAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) : Prop

Equality of two left cosets a + s and b + s.

def LeftCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) : Prop

Equality of two left cosets a * s and b * s.

theorem leftAddCosetEquivalence_rel {α : Type u_1} [Add α] (s : Set α) : Equivalence (LeftAddCosetEquivalence s)

theorem leftCosetEquivalence_rel {α : Type u_1} [Mul α] (s : Set α) : Equivalence (LeftCosetEquivalence s)

def RightAddCosetEquivalence {α : Type u_1} [Add α] (s : Set α) (a : α) (b : α) : Prop

Equality of two right cosets s + a and s + b.

def RightCosetEquivalence {α : Type u_1} [Mul α] (s : Set α) (a : α) (b : α) : Prop

Equality of two right cosets s * a and s * b.

theorem rightAddCosetEquivalence_rel {α : Type u_1} [Add α] (s : Set α) : Equivalence (RightAddCosetEquivalence s)

theorem rightCosetEquivalence_rel {α : Type u_1} [Mul α] (s : Set α) : Equivalence (RightCosetEquivalence s)

@[simp]

theorem leftAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) : leftAddCoset a (leftAddCoset b s) = leftAddCoset (a + b) s

@[simp]

theorem leftCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) : leftCoset a (leftCoset b s) = leftCoset (a * b) s

@[simp]

theorem rightAddCoset_assoc {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) : rightAddCoset (rightAddCoset s a) b = rightAddCoset s (a + b)

@[simp]

theorem rightCoset_assoc {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) : rightCoset (rightCoset s a) b = rightCoset s (a * b)

theorem leftAddCoset_rightAddCoset {α : Type u_1} [AddSemigroup α] (s : Set α) (a : α) (b : α) : rightAddCoset (leftAddCoset a s) b = leftAddCoset a (rightAddCoset s b)

theorem leftCoset_rightCoset {α : Type u_1} [Semigroup α] (s : Set α) (a : α) (b : α) : rightCoset (leftCoset a s) b = leftCoset a (rightCoset s b)

@[simp]

theorem zero_leftAddCoset {α : Type u_1} [AddMonoid α] (s : Set α) : leftAddCoset 0 s = s

@[simp]

theorem one_leftCoset {α : Type u_1} [Monoid α] (s : Set α) : leftCoset 1 s = s

@[simp]

theorem rightAddCoset_zero {α : Type u_1} [AddMonoid α] (s : Set α) : rightAddCoset s 0 = s

@[simp]

theorem rightCoset_one {α : Type u_1} [Monoid α] (s : Set α) : rightCoset s 1 = s

theorem mem_own_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) : a ∈ leftAddCoset a ↑s

theorem mem_own_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) : a ∈ leftCoset a ↑s

theorem mem_own_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) (a : α) : a ∈ rightAddCoset (↑s) a

theorem mem_own_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) (a : α) : a ∈ rightCoset (↑s) a

theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : leftAddCoset a ↑s = ↑s) : a ∈ s

theorem mem_leftCoset_leftCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : leftCoset a ↑s = ↑s) : a ∈ s

theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [AddMonoid α] (s : AddSubmonoid α) {a : α} (ha : rightAddCoset (↑s) a = ↑s) : a ∈ s

theorem mem_rightCoset_rightCoset {α : Type u_1} [Monoid α] (s : Submonoid α) {a : α} (ha : rightCoset (↑s) a = ↑s) : a ∈ s

theorem mem_leftAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) : x ∈ leftAddCoset a s ↔ -a + x ∈ s

abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) (motive : x ∈ leftAddCoset a s → Prop) : (x : x ∈ leftAddCoset a s) → ((b : α) → (hb : b ∈ s) → (Eq : (fun x => a + x) b = x) → motive (_ : ∃ a, a ∈ s ∧ (fun x => a + x) a = x)) → motive x

theorem mem_leftCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) : x ∈ leftCoset a s ↔ a⁻¹ * x ∈ s

theorem mem_rightAddCoset_iff {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) : x ∈ rightAddCoset s a ↔ x + -a ∈ s

abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [AddGroup α] {s : Set α} {x : α} (a : α) (motive : x ∈ rightAddCoset s a → Prop) : (x : x ∈ rightAddCoset s a) → ((b : α) → (hb : b ∈ s) → (Eq : (fun x => x + a) b = x) → motive (_ : ∃ a, a ∈ s ∧ (fun x => x + a) a = x)) → motive x

theorem mem_rightCoset_iff {α : Type u_1} [Group α] {s : Set α} {x : α} (a : α) : x ∈ rightCoset s a ↔ x * a⁻¹ ∈ s

theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : leftAddCoset a ↑s = ↑s

theorem leftCoset_mem_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a ∈ s) : leftCoset a ↑s = ↑s

theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : rightAddCoset (↑s) a = ↑s

theorem rightCoset_mem_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a ∈ s) : rightCoset (↑s) a = ↑s

abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b ∈ AddAction.orbit { x // x ∈ s } a → Prop) : (x : _b ∈ AddAction.orbit { x // x ∈ s } a) → ((c : { x // x ∈ s }) → (d : (fun m => m +ᵥ a) c = _b) → motive (_ : ∃ y, (fun m => m +ᵥ a) y = _b)) → motive x

abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (_b : α) (motive : _b ∈ rightAddCoset (↑s) a → Prop) : (x : _b ∈ rightAddCoset (↑s) a) → ((c : α) → (d : c ∈ ↑s) → (e : (fun x => x + a) c = _b) → motive (_ : ∃ a, a ∈ ↑s ∧ (fun x => x + a) a = _b)) → motive x

theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) : AddAction.orbit { x // x ∈ s } a = rightAddCoset (↑s) a

theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [Group α] (s : Subgroup α) (a : α) : MulAction.orbit { x // x ∈ s } a = rightCoset (↑s) a

theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {a : α} (ha : a ∈ s) : AddAction.orbit { x // x ∈ s } a = ↑s

theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [Group α] (s : Subgroup α) {a : α} (ha : a ∈ s) : MulAction.orbit { x // x ∈ s } a = ↑s

theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : AddAction.orbit { x // x ∈ s } 0 = ↑s

theorem orbit_subgroup_one_eq_self {α : Type u_1} [Group α] (s : Subgroup α) : MulAction.orbit { x // x ∈ s } 1 = ↑s

theorem eq_addCosets_of_normal {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (N : AddSubgroup.Normal s) (g : α) : leftAddCoset g ↑s = rightAddCoset (↑s) g

theorem eq_cosets_of_normal {α : Type u_1} [Group α] (s : Subgroup α) (N : Subgroup.Normal s) (g : α) : leftCoset g ↑s = rightCoset (↑s) g

theorem normal_of_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (h : ∀ (g : α), leftAddCoset g ↑s = rightAddCoset (↑s) g) : AddSubgroup.Normal s

theorem normal_of_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) (h : ∀ (g : α), leftCoset g ↑s = rightCoset (↑s) g) : Subgroup.Normal s

theorem normal_iff_eq_addCosets {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : AddSubgroup.Normal s ↔ ∀ (g : α), leftAddCoset g ↑s = rightAddCoset (↑s) g

theorem normal_iff_eq_cosets {α : Type u_1} [Group α] (s : Subgroup α) : Subgroup.Normal s ↔ ∀ (g : α), leftCoset g ↑s = rightCoset (↑s) g

theorem leftAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} : leftAddCoset x ↑s = leftAddCoset y ↑s ↔ -x + y ∈ s

theorem leftCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} : leftCoset x ↑s = leftCoset y ↑s ↔ x⁻¹ * y ∈ s

theorem rightAddCoset_eq_iff {α : Type u_1} [AddGroup α] (s : AddSubgroup α) {x : α} {y : α} : rightAddCoset (↑s) x = rightAddCoset (↑s) y ↔ y + -x ∈ s

theorem rightCoset_eq_iff {α : Type u_1} [Group α] (s : Subgroup α) {x : α} {y : α} : rightCoset (↑s) x = rightCoset (↑s) y ↔ y * x⁻¹ ∈ s

def QuotientAddGroup.leftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Setoid α

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

def QuotientGroup.leftRel {α : Type u_1} [Group α] (s : Subgroup α) : Setoid α

The equivalence relation corresponding to the partition of a group by left cosets of a subgroup.

theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x : α} {y : α} : Setoid.r x y ↔ -x + y ∈ s

theorem QuotientGroup.leftRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} : Setoid.r x y ↔ x⁻¹ * y ∈ s

theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Setoid.r = fun x y => -x + y ∈ s

theorem QuotientGroup.leftRel_eq {α : Type u_1} [Group α] (s : Subgroup α) : Setoid.r = fun x y => x⁻¹ * y ∈ s

theorem QuotientGroup.leftRel_r_eq_leftCosetEquivalence {α : Type u_1} [Group α] (s : Subgroup α) : Setoid.r = LeftCosetEquivalence ↑s

theorem QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) : Decidable (Setoid.r x y) = Decidable ((fun x y => -x + y ∈ s) x y)

instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun x => x ∈ s] : DecidableRel Setoid.r

instance QuotientGroup.leftRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun x => x ∈ s] : DecidableRel Setoid.r

instance QuotientAddGroup.instHasQuotientAddSubgroup {α : Type u_1} [AddGroup α] : HasQuotient α (AddSubgroup α)

α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

instance QuotientGroup.instHasQuotientSubgroup {α : Type u_1} [Group α] : HasQuotient α (Subgroup α)

α ⧸ s is the quotient type representing the left cosets of s. If s is a normal subgroup, α ⧸ s is a group

def QuotientAddGroup.rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Setoid α

The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

def QuotientGroup.rightRel {α : Type u_1} [Group α] (s : Subgroup α) : Setoid α

The equivalence relation corresponding to the partition of a group by right cosets of a subgroup.

theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {x : α} {y : α} : Setoid.r x y ↔ y + -x ∈ s

theorem QuotientGroup.rightRel_apply {α : Type u_1} [Group α] {s : Subgroup α} {x : α} {y : α} : Setoid.r x y ↔ y * x⁻¹ ∈ s

theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Setoid.r = fun x y => y + -x ∈ s

theorem QuotientGroup.rightRel_eq {α : Type u_1} [Group α] (s : Subgroup α) : Setoid.r = fun x y => y * x⁻¹ ∈ s

theorem QuotientGroup.rightRel_r_eq_rightCosetEquivalence {α : Type u_1} [Group α] (s : Subgroup α) : Setoid.r = RightCosetEquivalence ↑s

theorem QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (x : α) (y : α) : Decidable (Setoid.r x y) = Decidable ((fun x y => y + -x ∈ s) x y)

instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [DecidablePred fun x => x ∈ s] : DecidableRel Setoid.r

instance QuotientGroup.rightRelDecidable {α : Type u_1} [Group α] (s : Subgroup α) [DecidablePred fun x => x ∈ s] : DecidableRel Setoid.r

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : Quotient (QuotientAddGroup.rightRel s)) : Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)) (Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)) g) = g

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) : Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (a : α) (b : α) : Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)

def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Quotient (QuotientAddGroup.rightRel s) ≃ α ⧸ s

Right cosets are in bijection with left cosets.

theorem QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α ⧸ s) : Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)) (Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)) g) = g

def QuotientGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [Group α] (s : Subgroup α) : Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s

Right cosets are in bijection with left cosets.

instance QuotientAddGroup.fintypeQuotientRightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [Fintype (α ⧸ s)] : Fintype (Quotient (QuotientAddGroup.rightRel s))

instance QuotientGroup.fintypeQuotientRightRel {α : Type u_1} [Group α] (s : Subgroup α) [Fintype (α ⧸ s)] : Fintype (Quotient (QuotientGroup.rightRel s))

theorem QuotientAddGroup.card_quotient_rightRel {α : Type u_1} [AddGroup α] (s : AddSubgroup α) [Fintype (α ⧸ s)] : Fintype.card (Quotient (QuotientAddGroup.rightRel s)) = Fintype.card (α ⧸ s)

theorem QuotientGroup.card_quotient_rightRel {α : Type u_1} [Group α] (s : Subgroup α) [Fintype (α ⧸ s)] : Fintype.card (Quotient (QuotientGroup.rightRel s)) = Fintype.card (α ⧸ s)

instance QuotientAddGroup.fintype {α : Type u_1} [AddGroup α] [Fintype α] (s : AddSubgroup α) [DecidableRel Setoid.r] : Fintype (α ⧸ s)

instance QuotientGroup.fintype {α : Type u_1} [Group α] [Fintype α] (s : Subgroup α) [DecidableRel Setoid.r] : Fintype (α ⧸ s)

abbrev QuotientAddGroup.mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α) : α ⧸ s

The canonical map from an AddGroup α to the quotient α ⧸ s.

@[inline, reducible]

abbrev QuotientGroup.mk {α : Type u_1} [Group α] {s : Subgroup α} (a : α) : α ⧸ s

The canonical map from a group α to the quotient α ⧸ s.

theorem QuotientAddGroup.mk_surjective {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : Function.Surjective QuotientAddGroup.mk

theorem QuotientGroup.mk_surjective {α : Type u_1} [Group α] {s : Subgroup α} : Function.Surjective QuotientGroup.mk

@[simp]

theorem QuotientAddGroup.range_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : Set.range QuotientAddGroup.mk = Set.univ

@[simp]

theorem QuotientGroup.range_mk {α : Type u_1} [Group α] {s : Subgroup α} : Set.range QuotientGroup.mk = Set.univ

theorem QuotientAddGroup.induction_on {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : (z : α) → C ↑z) : C x

theorem QuotientGroup.induction_on {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : (z : α) → C ↑z) : C x

instance QuotientAddGroup.instCoeQuotientAddSubgroupInstHasQuotientAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : Coe α (α ⧸ s)

instance QuotientGroup.instCoeQuotientSubgroupInstHasQuotientSubgroup {α : Type u_1} [Group α] {s : Subgroup α} : Coe α (α ⧸ s)

theorem QuotientAddGroup.induction_on' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : (z : α) → C ↑z) : C x

theorem QuotientGroup.induction_on' {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s) (H : (z : α) → C ↑z) : C x

@[simp]

theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {β : Sort u_2} (f : α → β) (h : ∀ (a b : α), Setoid.r a b → f a = f b) (x : α) : Quotient.liftOn' (↑x) f h = f x

@[simp]

theorem QuotientGroup.quotient_liftOn_mk {α : Type u_1} [Group α] {s : Subgroup α} {β : Sort u_2} (f : α → β) (h : ∀ (a b : α), Setoid.r a b → f a = f b) (x : α) : Quotient.liftOn' (↑x) f h = f x

theorem QuotientAddGroup.forall_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} : ((x : α ⧸ s) → C x) ↔ (x : α) → C ↑x

theorem QuotientGroup.forall_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} : ((x : α ⧸ s) → C x) ↔ (x : α) → C ↑x

theorem QuotientAddGroup.exists_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {C : α ⧸ s → Prop} : (∃ x, C x) ↔ ∃ x, C ↑x

theorem QuotientGroup.exists_mk {α : Type u_1} [Group α] {s : Subgroup α} {C : α ⧸ s → Prop} : (∃ x, C x) ↔ ∃ x, C ↑x

instance QuotientAddGroup.instInhabitedQuotientAddSubgroupInstHasQuotientAddSubgroup {α : Type u_1} [AddGroup α] (s : AddSubgroup α) : Inhabited (α ⧸ s)

instance QuotientGroup.instInhabitedQuotientSubgroupInstHasQuotientSubgroup {α : Type u_1} [Group α] (s : Subgroup α) : Inhabited (α ⧸ s)

theorem QuotientAddGroup.eq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a : α} {b : α} : ↑a = ↑b ↔ -a + b ∈ s

theorem QuotientGroup.eq {α : Type u_1} [Group α] {s : Subgroup α} {a : α} {b : α} : ↑a = ↑b ↔ a⁻¹ * b ∈ s

theorem QuotientAddGroup.eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {a : α} {b : α} : ↑a = ↑b ↔ -a + b ∈ s

theorem QuotientGroup.eq' {α : Type u_1} [Group α] {s : Subgroup α} {a : α} {b : α} : ↑a = ↑b ↔ a⁻¹ * b ∈ s

theorem QuotientAddGroup.out_eq' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (a : α ⧸ s) : ↑(Quotient.out' a) = a

theorem QuotientGroup.out_eq' {α : Type u_1} [Group α] {s : Subgroup α} (a : α ⧸ s) : ↑(Quotient.out' a) = a

theorem QuotientAddGroup.mk_out'_eq_mul {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) : ∃ h, Quotient.out' ↑g = g + ↑h

theorem QuotientGroup.mk_out'_eq_mul {α : Type u_1} [Group α] (s : Subgroup α) (g : α) : ∃ h, Quotient.out' ↑g = g * ↑h

@[simp]

theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {b : α} (a : α) (hb : b ∈ s) : ↑(a + b) = ↑a

@[simp]

theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [Group α] {s : Subgroup α} {b : α} (a : α) (hb : b ∈ s) : ↑(a * b) = ↑a

theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (g : α) : {x | ↑x = ↑g} = leftAddCoset g ↑s

theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [Group α] (s : Subgroup α) (g : α) : {x | ↑x = ↑g} = leftCoset g ↑s

theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) : QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 + ↑x) ⁻¹' s

abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (∃ x, x ∈ N ∧ x + x ∈ s) → Prop) : (x : ∃ x, x ∈ N ∧ x + x ∈ s) → ((z : α) → (hz : z ∈ N) → (hxz : x + z ∈ s) → motive (_ : ∃ x, x ∈ N ∧ x + x ∈ s)) → motive x

abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) (x : α) (motive : (∃ x, x ∈ s ∧ -x + x ∈ N) → Prop) : (x : ∃ x, x ∈ s ∧ -x + x ∈ N) → ((y : α) → (hs : y ∈ s) → (hN : -y + x ∈ N) → motive (_ : ∃ x, x ∈ s ∧ -x + x ∈ N)) → motive x

theorem QuotientGroup.preimage_image_mk {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) : QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) ⁻¹' s

theorem QuotientAddGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [AddGroup α] (N : AddSubgroup α) (s : Set α) : QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 + ↑x) '' s

theorem QuotientGroup.preimage_image_mk_eq_iUnion_image {α : Type u_1} [Group α] (N : Subgroup α) (s : Set α) : QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) '' s

abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (motive : { x // x ∈ s } → Prop) : (x : { x // x ∈ s }) → ((g : α) → (hg : g ∈ s) → motive { val := g, property := hg }) → motive x

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : ↑(leftAddCoset g ↑s)) : -g + ↑x ∈ ↑s

def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ↑(leftAddCoset g ↑s) ≃ { x // x ∈ s }

The natural bijection between the cosets g + s and s.

abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (motive : ↑(leftAddCoset g ↑s) → Prop) : (x : ↑(leftAddCoset g ↑s)) → ((x : α) → (hx : x ∈ leftAddCoset g ↑s) → motive { val := x, property := hx }) → motive x

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : { x // x ∈ s }), (fun x => { val := -g + ↑x, property := (_ : -g + ↑x ∈ ↑s) }) ((fun x => { val := g + ↑x, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => g + x) a = g + ↑x) }) x) = x

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : ↑(leftAddCoset g ↑s)), (fun x => { val := g + ↑x, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => g + x) a = g + ↑x) }) ((fun x => { val := -g + ↑x, property := (_ : -g + ↑x ∈ ↑s) }) x) = x

theorem AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : { x // x ∈ s }) : ∃ a, a ∈ ↑s ∧ (fun x => g + x) a = g + ↑x

def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : ↑(leftCoset g ↑s) ≃ { x // x ∈ s }

The natural bijection between a left coset g * s and s.

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : ↑(rightAddCoset (↑s) g)) : ↑x + -g ∈ ↑s

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : { x // x ∈ s }), (fun x => { val := ↑x + -g, property := (_ : ↑x + -g ∈ ↑s) }) ((fun x => { val := ↑x + g, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => x + g) a = ↑x + g) }) x) = x

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ∀ (x : ↑(rightAddCoset (↑s) g)), (fun x => { val := ↑x + g, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => x + g) a = ↑x + g) }) ((fun x => { val := ↑x + -g, property := (_ : ↑x + -g ∈ ↑s) }) x) = x

theorem AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (x : { x // x ∈ s }) : ∃ a, a ∈ ↑s ∧ (fun x => x + g) a = ↑x + g

abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) (motive : ↑(rightAddCoset (↑s) g) → Prop) : (x : ↑(rightAddCoset (↑s) g)) → ((x : α) → (hx : x ∈ rightAddCoset (↑s) g) → motive { val := x, property := hx }) → motive x

def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (g : α) : ↑(rightAddCoset (↑s) g) ≃ { x // x ∈ s }

The natural bijection between the cosets s + g and s.

def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [Group α] {s : Subgroup α} (g : α) : ↑(rightCoset (↑s) g) ≃ { x // x ∈ s }

The natural bijection between a right coset s * g and s.

theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α ⧸ s) : ({ x // ↑x = L } ≃ ↑(leftAddCoset (Quotient.out' L) ↑s)) = ({ x // ↑x = L } ≃ ↑{x | ↑x = ↑(Quotient.out' L)})

theorem AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} (L : α ⧸ s) : ({ x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = Quotient.mk'' (Quotient.out' L) }) = ({ x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = L })

noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [AddGroup α] {s : AddSubgroup α} : α ≃ (α ⧸ s) × { x // x ∈ s }

A (non-canonical) bijection between an add_group α and the product (α/s) × s

noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [Group α] {s : Subgroup α} : α ≃ (α ⧸ s) × { x // x ∈ s }

A (non-canonical) bijection between a group α and the product (α/s) × s

def AddSubgroup.quotientEquivOfEq {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) : α ⧸ s ≃ α ⧸ t

If two subgroups M and N of G are equal, their quotients are in bijection.

theorem AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) : Setoid.r (id _a) (id _b)

theorem AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α ⧸ s) : Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _b → Setoid.r (id _a) (id _b)) (Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _b → Setoid.r (id _a) (id _b)) q) = q

theorem AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) : Setoid.r (id _a) (id _b)

theorem AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s = t) (q : α ⧸ t) : Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _b → Setoid.r (id _a) (id _b)) (Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _b → Setoid.r (id _a) (id _b)) q) = q

def Subgroup.quotientEquivOfEq {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) : α ⧸ s ≃ α ⧸ t

If two subgroups M and N of G are equal, their quotients are in bijection.

theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s = t) (a : α) : ↑(Subgroup.quotientEquivOfEq h) ↑a = ↑a

theorem AddSubgroup.quotientEquivSumOfLE'.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (b : α) (c : α) (h : Setoid.r b c) : Setoid.r (id b) (id c)

theorem AddSubgroup.quotientEquivSumOfLE'.proof_6 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (t : (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t) : (fun a => (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) (_ : ∀ (b c : α), Setoid.r b c → Setoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) c)) a)) ((fun a => Quotient.map' (fun b => f a.fst + ↑b) (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst + ↑b) b) ((fun b => f a.fst + ↑b) c)) a.snd) t) = t

def AddSubgroup.quotientEquivSumOfLE' {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) : α ⧸ s ≃ (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t

If H ≤ K, then G/H ≃ G/K × K/H constructively, using the provided right inverse of the quotient map G → G/K. The classical version is AddSubgroup.quotientEquivSumOfLE.

theorem AddSubgroup.quotientEquivSumOfLE'.proof_4 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (f : α ⧸ t → α) (a : (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t) (b : { x // x ∈ t }) (c : { x // x ∈ t }) (h : Setoid.r b c) : Setoid.r ((fun b => f a.fst + ↑b) b) ((fun b => f a.fst + ↑b) c)

theorem AddSubgroup.quotientEquivSumOfLE'.proof_3 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (b : α) (c : α) (h : Setoid.r b c) : Setoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) c)

theorem AddSubgroup.quotientEquivSumOfLE'.proof_2 {α : Type u_1} [AddGroup α] {t : AddSubgroup α} (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) : -f (Quotient.mk'' g) + g ∈ t

theorem AddSubgroup.quotientEquivSumOfLE'.proof_5 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : Quotient (QuotientAddGroup.leftRel s)) : (fun a => Quotient.map' (fun b => f a.fst + ↑b) (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst + ↑b) b) ((fun b => f a.fst + ↑b) c)) a.snd) ((fun a => (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) (_ : ∀ (b c : α), Setoid.r b c → Setoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) c)) a)) q) = q

@[simp]

theorem Subgroup.quotientEquivProdOfLE'_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) (a : α ⧸ s) : ↑(Subgroup.quotientEquivProdOfLE' h_le f hf) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) (_ : ∀ (b c : α), Setoid.r b c → Setoid.r ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b) ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) c)) a)

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE'_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α ⧸ s) : ↑(AddSubgroup.quotientEquivSumOfLE' h_le f hf) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) (_ : ∀ (b c : α), Setoid.r b c → Setoid.r ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) b) ((fun g => { val := -f (Quotient.mk'' g) + g, property := (_ : -f (Quotient.mk'' g) + g ∈ t) }) c)) a)

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE'_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t) : ↑(AddSubgroup.quotientEquivSumOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.fst + ↑b) (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst + ↑b) b) ((fun b => f a.fst + ↑b) c)) a.snd

@[simp]

theorem Subgroup.quotientEquivProdOfLE'_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α ⧸ t) × { x // x ∈ t } ⧸ Subgroup.subgroupOf s t) : ↑(Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.fst * ↑b) (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c)) a.snd

def Subgroup.quotientEquivProdOfLE' {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) : α ⧸ s ≃ (α ⧸ t) × { x // x ∈ t } ⧸ Subgroup.subgroupOf s t

If H ≤ K, then G/H ≃ G/K × K/H constructively, using the provided right inverse of the quotient map G → G/K. The classical version is Subgroup.quotientEquivProdOfLE.

noncomputable def AddSubgroup.quotientEquivSumOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

theorem AddSubgroup.quotientEquivSumOfLE.proof_1 {α : Type u_1} [AddGroup α] {t : AddSubgroup α} (q : Quotient (QuotientAddGroup.leftRel t)) : Quotient.mk'' (Quotient.out' q) = q

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE_symm_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t) : ↑(AddSubgroup.quotientEquivSumOfLE h_le).symm a = Quotient.map' (fun b => Quotient.out' a.fst + ↑b) (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => Quotient.out' a.fst + ↑b) b) ((fun b => Quotient.out' a.fst + ↑b) c)) a.snd

@[simp]

theorem AddSubgroup.quotientEquivSumOfLE_apply {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (a : α ⧸ s) : ↑(AddSubgroup.quotientEquivSumOfLE h_le) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -Quotient.out' (Quotient.mk'' g) + g, property := (_ : -Quotient.out' (Quotient.mk'' g) + g ∈ t) }) (_ : ∀ (b c : α), Setoid.r b c → Setoid.r ((fun g => { val := -Quotient.out' (Quotient.mk'' g) + g, property := (_ : -Quotient.out' (Quotient.mk'' g) + g ∈ t) }) b) ((fun g => { val := -Quotient.out' (Quotient.mk'' g) + g, property := (_ : -Quotient.out' (Quotient.mk'' g) + g ∈ t) }) c)) a)

@[simp]

theorem Subgroup.quotientEquivProdOfLE_symm_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × { x // x ∈ t } ⧸ Subgroup.subgroupOf s t) : ↑(Subgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun b => Quotient.out' a.fst * ↑b) (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => Quotient.out' a.fst * ↑b) b) ((fun b => Quotient.out' a.fst * ↑b) c)) a.snd

@[simp]

theorem Subgroup.quotientEquivProdOfLE_apply {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (a : α ⧸ s) : ↑(Subgroup.quotientEquivProdOfLE h_le) a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := (Quotient.out' (Quotient.mk'' g))⁻¹ * g, property := (_ : (Quotient.out' (Quotient.mk'' g))⁻¹ * g ∈ t) }) (_ : ∀ (b c : α), Setoid.r b c → Setoid.r ((fun g => { val := (Quotient.out' (Quotient.mk'' g))⁻¹ * g, property := (_ : (Quotient.out' (Quotient.mk'' g))⁻¹ * g ∈ t) }) b) ((fun g => { val := (Quotient.out' (Quotient.mk'' g))⁻¹ * g, property := (_ : (Quotient.out' (Quotient.mk'' g))⁻¹ * g ∈ t) }) c)) a)

noncomputable def Subgroup.quotientEquivProdOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × { x // x ∈ t } ⧸ Subgroup.subgroupOf s t

If H ≤ K, then G/H ≃ G/K × K/H nonconstructively. The constructive version is quotientEquivProdOfLE'.

def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) : { x // x ∈ s } ⧸ AddSubgroup.addSubgroupOf H s ↪ { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf H t

If s ≤ t, then there is an embedding s ⧸ H.addSubgroupOf s ↪ t ⧸ H.addSubgroupOf t.

theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_2 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (q₁ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf H s))) (q₂ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf H s))) : Quotient.map' ↑(AddSubgroup.inclusion h) (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)) q₁ = Quotient.map' ↑(AddSubgroup.inclusion h) (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)) q₂ → q₁ = q₂

theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (a : { x // x ∈ s }) (b : { x // x ∈ s }) : Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)

def Subgroup.quotientSubgroupOfEmbeddingOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) : { x // x ∈ s } ⧸ Subgroup.subgroupOf H s ↪ { x // x ∈ t } ⧸ Subgroup.subgroupOf H t

If s ≤ t, then there is an embedding s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t.

@[simp]

theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (g : { x // x ∈ s }) : ↑(AddSubgroup.quotientAddSubgroupOfEmbeddingOfLE H h) ↑g = ↑(↑(AddSubgroup.inclusion h) g)

@[simp]

theorem Subgroup.quotientSubgroupOfEmbeddingOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : { x // x ∈ s }) : ↑(Subgroup.quotientSubgroupOfEmbeddingOfLE H h) ↑g = ↑(↑(Subgroup.inclusion h) g)

def AddSubgroup.quotientAddSubgroupOfMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) : { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf s H → { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf t H

If s ≤ t, then there is a map H ⧸ s.addSubgroupOf H → H ⧸ t.addSubgroupOf H.

theorem AddSubgroup.quotientAddSubgroupOfMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (a : { x // x ∈ H }) (b : { x // x ∈ H }) : Setoid.r a b → Setoid.r (id a) (id b)

def Subgroup.quotientSubgroupOfMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) : { x // x ∈ H } ⧸ Subgroup.subgroupOf s H → { x // x ∈ H } ⧸ Subgroup.subgroupOf t H

If s ≤ t, then there is a map H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H.

@[simp]

theorem AddSubgroup.quotientAddSubgroupOfMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (g : { x // x ∈ H }) : AddSubgroup.quotientAddSubgroupOfMapOfLE H h ↑g = ↑g

@[simp]

theorem Subgroup.quotientSubgroupOfMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (H : Subgroup α) (h : s ≤ t) (g : { x // x ∈ H }) : Subgroup.quotientSubgroupOfMapOfLE H h ↑g = ↑g

theorem AddSubgroup.quotientMapOfLE.proof_1 {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) (a : α) (b : α) : Setoid.r a b → Setoid.r (id a) (id b)

def AddSubgroup.quotientMapOfLE {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) : α ⧸ s → α ⧸ t

If s ≤ t, then there is a map α ⧸ s → α ⧸ t.

def Subgroup.quotientMapOfLE {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s ≤ t) : α ⧸ s → α ⧸ t

If s ≤ t, then there is a map α ⧸ s → α ⧸ t.

@[simp]

theorem AddSubgroup.quotientMapOfLE_apply_mk {α : Type u_1} [AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h : s ≤ t) (g : α) : AddSubgroup.quotientMapOfLE h ↑g = ↑g

@[simp]

theorem Subgroup.quotientMapOfLE_apply_mk {α : Type u_1} [Group α] {s : Subgroup α} {t : Subgroup α} (h : s ≤ t) (g : α) : Subgroup.quotientMapOfLE h ↑g = ↑g

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (i : ι) : iInf f ≤ f i

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf (⨅ (i : ι), f i) H))) (q₂ : Quotient (QuotientAddGroup.leftRel (AddSubgroup.addSubgroupOf (⨅ (i : ι), f i) H))) : (fun q i => AddSubgroup.quotientAddSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q) q₁ = (fun q i => AddSubgroup.quotientAddSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q) q₂ → q₁ = q₂

def AddSubgroup.quotientiInfAddSubgroupOfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) : { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf (⨅ (i : ι), f i) H ↪ (i : ι) → { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf (f i) H

The natural embedding H ⧸ (⨅ i, f i).addSubgroupOf H) ↪ Π i, H ⧸ (f i).addSubgroupOf H.

@[simp]

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (q : { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf (⨅ (i : ι), f i) H) (i : ι) : ↑(AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) q i = AddSubgroup.quotientAddSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q

@[simp]

theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) (q : { x // x ∈ H } ⧸ Subgroup.subgroupOf (⨅ (i : ι), f i) H) (i : ι) : ↑(Subgroup.quotientiInfSubgroupOfEmbedding f H) q i = Subgroup.quotientSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q

def Subgroup.quotientiInfSubgroupOfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) : { x // x ∈ H } ⧸ Subgroup.subgroupOf (⨅ (i : ι), f i) H ↪ (i : ι) → { x // x ∈ H } ⧸ Subgroup.subgroupOf (f i) H

The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H.

@[simp]

theorem AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (g : { x // x ∈ H }) (i : ι) : ↑(AddSubgroup.quotientiInfAddSubgroupOfEmbedding f H) (↑g) i = ↑g

@[simp]

theorem Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) (g : { x // x ∈ H }) (i : ι) : ↑(Subgroup.quotientiInfSubgroupOfEmbedding f H) (↑g) i = ↑g

theorem AddSubgroup.quotientiInfEmbedding.proof_1 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (i : ι) : iInf f ≤ f i

theorem AddSubgroup.quotientiInfEmbedding.proof_2 {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (q₁ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (⨅ (i : ι), f i))) : (fun q i => AddSubgroup.quotientMapOfLE (_ : iInf f ≤ f i) q) q₁ = (fun q i => AddSubgroup.quotientMapOfLE (_ : iInf f ≤ f i) q) q₂ → q₁ = q₂

def AddSubgroup.quotientiInfEmbedding {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) : α ⧸ ⨅ (i : ι), f i ↪ (i : ι) → α ⧸ f i

The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i.

@[simp]

theorem AddSubgroup.quotientiInfEmbedding_apply {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (q : α ⧸ ⨅ (i : ι), f i) (i : ι) : ↑(AddSubgroup.quotientiInfEmbedding f) q i = AddSubgroup.quotientMapOfLE (_ : iInf f ≤ f i) q

@[simp]

theorem Subgroup.quotientiInfEmbedding_apply {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (q : α ⧸ ⨅ (i : ι), f i) (i : ι) : ↑(Subgroup.quotientiInfEmbedding f) q i = Subgroup.quotientMapOfLE (_ : iInf f ≤ f i) q

def Subgroup.quotientiInfEmbedding {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) : α ⧸ ⨅ (i : ι), f i ↪ (i : ι) → α ⧸ f i

The natural embedding α ⧸ (⨅ i, f i) ↪ Π i, α ⧸ f i.

@[simp]

theorem AddSubgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (g : α) (i : ι) : ↑(AddSubgroup.quotientiInfEmbedding f) (↑g) i = ↑g

@[simp]

theorem Subgroup.quotientiInfEmbedding_apply_mk {α : Type u_1} [Group α] {ι : Type u_2} (f : ι → Subgroup α) (g : α) (i : ι) : ↑(Subgroup.quotientiInfEmbedding f) (↑g) i = ↑g

theorem AddSubgroup.card_eq_card_quotient_add_card_addSubgroup {α : Type u_1} [AddGroup α] [Fintype α] (s : AddSubgroup α) [Fintype { x // x ∈ s }] [DecidablePred fun a => a ∈ s] : Fintype.card α = Fintype.card (α ⧸ s) * Fintype.card { x // x ∈ s }

theorem Subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [Group α] [Fintype α] (s : Subgroup α) [Fintype { x // x ∈ s }] [DecidablePred fun a => a ∈ s] : Fintype.card α = Fintype.card (α ⧸ s) * Fintype.card { x // x ∈ s }

theorem AddSubgroup.card_addSubgroup_dvd_card {α : Type u_1} [AddGroup α] [Fintype α] (s : AddSubgroup α) [Fintype { x // x ∈ s }] : Fintype.card { x // x ∈ s } ∣ Fintype.card α

Lagrange's Theorem: The order of an additive subgroup divides the order of its ambient additive group.

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [Group α] [Fintype α] (s : Subgroup α) [Fintype { x // x ∈ s }] : Fintype.card { x // x ∈ s } ∣ Fintype.card α

Lagrange's Theorem: The order of a subgroup divides the order of its ambient group.

theorem AddSubgroup.card_quotient_dvd_card {α : Type u_1} [AddGroup α] [Fintype α] (s : AddSubgroup α) [DecidablePred fun x => x ∈ s] : Fintype.card (α ⧸ s) ∣ Fintype.card α

theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [Group α] [Fintype α] (s : Subgroup α) [DecidablePred fun x => x ∈ s] : Fintype.card (α ⧸ s) ∣ Fintype.card α

theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] [Fintype α] [Fintype H] (f : α →+ H) (hf : Function.Injective ↑f) : Fintype.card α ∣ Fintype.card H

theorem Subgroup.card_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] [Fintype α] [Fintype H] (f : α →* H) (hf : Function.Injective ↑f) : Fintype.card α ∣ Fintype.card H

theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [AddGroup α] {H : AddSubgroup α} {K : AddSubgroup α} [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] (hHK : H ≤ K) : Fintype.card { x // x ∈ H } ∣ Fintype.card { x // x ∈ K }

theorem Subgroup.card_dvd_of_le {α : Type u_1} [Group α] {H : Subgroup α} {K : Subgroup α} [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] (hHK : H ≤ K) : Fintype.card { x // x ∈ H } ∣ Fintype.card { x // x ∈ K }

theorem AddSubgroup.card_comap_dvd_of_injective {α : Type u_1} [AddGroup α] {H : Type u_2} [AddGroup H] (K : AddSubgroup H) [Fintype { x // x ∈ K }] (f : α →+ H) [Fintype { x // x ∈ AddSubgroup.comap f K }] (hf : Function.Injective ↑f) : Fintype.card { x // x ∈ AddSubgroup.comap f K } ∣ Fintype.card { x // x ∈ K }

theorem Subgroup.card_comap_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (K : Subgroup H) [Fintype { x // x ∈ K }] (f : α →* H) [Fintype { x // x ∈ Subgroup.comap f K }] (hf : Function.Injective ↑f) : Fintype.card { x // x ∈ Subgroup.comap f K } ∣ Fintype.card { x // x ∈ K }

abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (motive : ↑(QuotientAddGroup.mk ⁻¹' t) → Prop) : (x : ↑(QuotientAddGroup.mk ⁻¹' t)) → ((a : α) → (ha : a ∈ QuotientAddGroup.mk ⁻¹' t) → motive { val := a, property := ha }) → motive x

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) : ↑a ∈ QuotientAddGroup.mk ⁻¹' t

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) : -Quotient.out' ↑↑a + ↑a ∈ s

noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) : ↑(QuotientAddGroup.mk ⁻¹' t) ≃ { x // x ∈ s } × ↑t

If s is a subgroup of the additive group α, and t is a subset of α ⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t.

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (a : { x // x ∈ s } × ↑t) : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t

abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) (motive : { x // x ∈ s } × ↑t → Prop) : (x : { x // x ∈ s } × ↑t) → ((a : α) → (ha : a ∈ s) → (x : α ⧸ s) → (hx : x ∈ t) → motive ({ val := a, property := ha }, { val := x, property := hx })) → motive x

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) : ∀ (x : { x // x ∈ s } × ↑t), (fun a => ({ val := -Quotient.out' ↑↑a + ↑a, property := (_ : -Quotient.out' ↑↑a + ↑a ∈ s) }, { val := ↑↑a, property := (_ : ↑a ∈ QuotientAddGroup.mk ⁻¹' t) })) ((fun a => { val := Quotient.out' ↑a.snd + ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t) }) x) = x

theorem QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [AddGroup α] (s : AddSubgroup α) (t : Set (α ⧸ s)) : ∀ (x : ↑(QuotientAddGroup.mk ⁻¹' t)), (fun a => { val := Quotient.out' ↑a.snd + ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t) }) ((fun a => ({ val := -Quotient.out' ↑↑a + ↑a, property := (_ : -Quotient.out' ↑↑a + ↑a ∈ s) }, { val := ↑↑a, property := (_ : ↑a ∈ QuotientAddGroup.mk ⁻¹' t) })) x) = x

noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [Group α] (s : Subgroup α) (t : Set (α ⧸ s)) : ↑(QuotientGroup.mk ⁻¹' t) ≃ { x // x ∈ s } × ↑t

If s is a subgroup of the group α, and t is a subset of α ⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t.