# Documentation

Mathlib.GroupTheory.Coset

# 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⧸ H is the quotient of the (additive) group G by the (additive) subgroup H

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

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

Equations
• = (fun x => a + x) '' s
def leftCoset {α : Type u_1} [inst : Mul α] (a : α) (s : Set α) :
Set α

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

Equations
• = (fun x => a * x) '' s
def rightAddCoset {α : Type u_1} [inst : Add α] (s : Set α) (a : α) :
Set α

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

Equations
• = (fun x => x + a) '' s
def rightCoset {α : Type u_1} [inst : Mul α] (s : Set α) (a : α) :
Set α

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

Equations
• = (fun x => x * a) '' s

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

Equations

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

Equations

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

Equations

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

Equations
theorem mem_leftAddCoset {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a + x
theorem mem_leftCoset {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
a * x
theorem mem_rightAddCoset {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α) (hxS : x s) :
x + a
theorem mem_rightCoset {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α) (hxS : x s) :
x * a
def LeftAddCosetEquivalence {α : Type u_1} [inst : Add α] (s : Set α) (a : α) (b : α) :

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

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

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

Equations
theorem leftAddCosetEquivalence_rel {α : Type u_1} [inst : Add α] (s : Set α) :
theorem leftCosetEquivalence_rel {α : Type u_1} [inst : Mul α] (s : Set α) :
def RightAddCosetEquivalence {α : Type u_1} [inst : Add α] (s : Set α) (a : α) (b : α) :

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

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

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

Equations
theorem rightAddCosetEquivalence_rel {α : Type u_1} [inst : Add α] (s : Set α) :
theorem rightCosetEquivalence_rel {α : Type u_1} [inst : Mul α] (s : Set α) :
@[simp]
theorem leftAddCoset_assoc {α : Type u_1} [inst : ] (s : Set α) (a : α) (b : α) :
@[simp]
theorem leftCoset_assoc {α : Type u_1} [inst : ] (s : Set α) (a : α) (b : α) :
leftCoset a () = leftCoset (a * b) s
@[simp]
theorem rightAddCoset_assoc {α : Type u_1} [inst : ] (s : Set α) (a : α) (b : α) :
@[simp]
theorem rightCoset_assoc {α : Type u_1} [inst : ] (s : Set α) (a : α) (b : α) :
rightCoset () b = rightCoset s (a * b)
theorem leftAddCoset_rightAddCoset {α : Type u_1} [inst : ] (s : Set α) (a : α) (b : α) :
theorem leftCoset_rightCoset {α : Type u_1} [inst : ] (s : Set α) (a : α) (b : α) :
@[simp]
theorem zero_leftAddCoset {α : Type u_1} [inst : ] (s : Set α) :
= s
@[simp]
theorem one_leftCoset {α : Type u_1} [inst : ] (s : Set α) :
= s
@[simp]
theorem rightAddCoset_zero {α : Type u_1} [inst : ] (s : Set α) :
= s
@[simp]
theorem rightCoset_one {α : Type u_1} [inst : ] (s : Set α) :
= s
theorem mem_own_leftAddCoset {α : Type u_1} [inst : ] (s : ) (a : α) :
a leftAddCoset a s
theorem mem_own_leftCoset {α : Type u_1} [inst : ] (s : ) (a : α) :
a leftCoset a s
theorem mem_own_rightAddCoset {α : Type u_1} [inst : ] (s : ) (a : α) :
a rightAddCoset (s) a
theorem mem_own_rightCoset {α : Type u_1} [inst : ] (s : ) (a : α) :
a rightCoset (s) a
theorem mem_leftAddCoset_leftAddCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : leftAddCoset a s = s) :
a s
theorem mem_leftCoset_leftCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : leftCoset a s = s) :
a s
theorem mem_rightAddCoset_rightAddCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : rightAddCoset (s) a = s) :
a s
theorem mem_rightCoset_rightCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : rightCoset (s) a = s) :
a s
abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [inst : ] {s : Set α} {x : α} (a : α) (motive : x Prop) :
(x : x ) → ((b : α) → (hb : b s) → (Eq : (fun x => a + x) b = x) → motive (_ : a, a s (fun x => a + x) a = x)) → motive x
Equations
theorem mem_leftAddCoset_iff {α : Type u_1} [inst : ] {s : Set α} {x : α} (a : α) :
x -a + x s
theorem mem_leftCoset_iff {α : Type u_1} [inst : ] {s : Set α} {x : α} (a : α) :
x a⁻¹ * x s
abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [inst : ] {s : Set α} {x : α} (a : α) (motive : x Prop) :
(x : x ) → ((b : α) → (hb : b s) → (Eq : (fun x => x + a) b = x) → motive (_ : a, a s (fun x => x + a) a = x)) → motive x
Equations
theorem mem_rightAddCoset_iff {α : Type u_1} [inst : ] {s : Set α} {x : α} (a : α) :
x x + -a s
theorem mem_rightCoset_iff {α : Type u_1} [inst : ] {s : Set α} {x : α} (a : α) :
x x * a⁻¹ s
theorem leftAddCoset_mem_leftAddCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : a s) :
leftAddCoset a s = s
theorem leftCoset_mem_leftCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : a s) :
leftCoset a s = s
theorem rightAddCoset_mem_rightAddCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : a s) :
rightAddCoset (s) a = s
theorem rightCoset_mem_rightCoset {α : Type u_1} [inst : ] (s : ) {a : α} (ha : a s) :
rightCoset (s) a = s
abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [inst : ] (s : ) (a : α) (_b : α) (motive : _b rightAddCoset (s) aProp) :
(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
Equations
abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [inst : ] (s : ) (a : α) (_b : α) (motive : _b AddAction.orbit { x // x s } aProp) :
(x : _b AddAction.orbit { x // x s } a) → ((c : { x // x s }) → (d : (fun x => x +ᵥ a) c = _b) → motive (_ : y, (fun x => x +ᵥ a) y = _b)) → motive x
Equations
theorem orbit_addSubgroup_eq_rightCoset {α : Type u_1} [inst : ] (s : ) (a : α) :
AddAction.orbit { x // x s } a = rightAddCoset (s) a
theorem orbit_subgroup_eq_rightCoset {α : Type u_1} [inst : ] (s : ) (a : α) :
MulAction.orbit { x // x s } a = rightCoset (s) a
theorem orbit_addSubgroup_eq_self_of_mem {α : Type u_1} [inst : ] (s : ) {a : α} (ha : a s) :
AddAction.orbit { x // x s } a = s
theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [inst : ] (s : ) {a : α} (ha : a s) :
MulAction.orbit { x // x s } a = s
theorem orbit_addSubgroup_zero_eq_self {α : Type u_1} [inst : ] (s : ) :
AddAction.orbit { x // x s } 0 = s
theorem orbit_subgroup_one_eq_self {α : Type u_1} [inst : ] (s : ) :
MulAction.orbit { x // x s } 1 = s
theorem eq_addCosets_of_normal {α : Type u_1} [inst : ] (s : ) (N : ) (g : α) :
leftAddCoset g s = rightAddCoset (s) g
theorem eq_cosets_of_normal {α : Type u_1} [inst : ] (s : ) (N : ) (g : α) :
leftCoset g s = rightCoset (s) g
theorem normal_of_eq_addCosets {α : Type u_1} [inst : ] (s : ) (h : ∀ (g : α), leftAddCoset g s = rightAddCoset (s) g) :
theorem normal_of_eq_cosets {α : Type u_1} [inst : ] (s : ) (h : ∀ (g : α), leftCoset g s = rightCoset (s) g) :
theorem normal_iff_eq_addCosets {α : Type u_1} [inst : ] (s : ) :
∀ (g : α), leftAddCoset g s = rightAddCoset (s) g
theorem normal_iff_eq_cosets {α : Type u_1} [inst : ] (s : ) :
∀ (g : α), leftCoset g s = rightCoset (s) g
theorem leftAddCoset_eq_iff {α : Type u_1} [inst : ] (s : ) {x : α} {y : α} :
leftAddCoset x s = leftAddCoset y s -x + y s
theorem leftCoset_eq_iff {α : Type u_1} [inst : ] (s : ) {x : α} {y : α} :
leftCoset x s = leftCoset y s x⁻¹ * y s
theorem rightAddCoset_eq_iff {α : Type u_1} [inst : ] (s : ) {x : α} {y : α} :
rightAddCoset (s) x = rightAddCoset (s) y y + -x s
theorem rightCoset_eq_iff {α : Type u_1} [inst : ] (s : ) {x : α} {y : α} :
rightCoset (s) x = rightCoset (s) y y * x⁻¹ s
def QuotientAddGroup.leftRel {α : Type u_1} [inst : ] (s : ) :

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

Equations
def QuotientGroup.leftRel {α : Type u_1} [inst : ] (s : ) :

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

Equations
theorem QuotientAddGroup.leftRel_apply {α : Type u_1} [inst : ] {s : } {x : α} {y : α} :
Setoid.r x y -x + y s
theorem QuotientGroup.leftRel_apply {α : Type u_1} [inst : ] {s : } {x : α} {y : α} :
theorem QuotientAddGroup.leftRel_eq {α : Type u_1} [inst : ] (s : ) :
Setoid.r = fun x y => -x + y s
theorem QuotientGroup.leftRel_eq {α : Type u_1} [inst : ] (s : ) :
Setoid.r = fun x y => x⁻¹ * y s
theorem QuotientGroup.leftRel_r_eq_leftCosetEquivalence {α : Type u_1} [inst : ] (s : ) :
Setoid.r =
def QuotientAddGroup.leftRelDecidable.proof_1 {α : Type u_1} [inst : ] (s : ) (x : α) (y : α) :
Decidable (Setoid.r x y) = Decidable ((fun x y => -x + y s) x y)
Equations
instance QuotientAddGroup.leftRelDecidable {α : Type u_1} [inst : ] (s : ) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
instance QuotientGroup.leftRelDecidable {α : Type u_1} [inst : ] (s : ) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
instance QuotientAddGroup.instHasQuotientAddSubgroup {α : Type u_1} [inst : ] :

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

Equations
• QuotientAddGroup.instHasQuotientAddSubgroup = { quotient' := fun s => }
instance QuotientGroup.instHasQuotientSubgroup {α : Type u_1} [inst : ] :

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

Equations
• QuotientGroup.instHasQuotientSubgroup = { quotient' := fun s => }
def QuotientAddGroup.rightRel {α : Type u_1} [inst : ] (s : ) :

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

Equations
def QuotientGroup.rightRel {α : Type u_1} [inst : ] (s : ) :

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

Equations
theorem QuotientAddGroup.rightRel_apply {α : Type u_1} [inst : ] {s : } {x : α} {y : α} :
Setoid.r x y y + -x s
theorem QuotientGroup.rightRel_apply {α : Type u_1} [inst : ] {s : } {x : α} {y : α} :
theorem QuotientAddGroup.rightRel_eq {α : Type u_1} [inst : ] (s : ) :
Setoid.r = fun x y => y + -x s
theorem QuotientGroup.rightRel_eq {α : Type u_1} [inst : ] (s : ) :
Setoid.r = fun x y => y * x⁻¹ s
theorem QuotientGroup.rightRel_r_eq_rightCosetEquivalence {α : Type u_1} [inst : ] (s : ) :
Setoid.r =
instance QuotientAddGroup.rightRelDecidable {α : Type u_1} [inst : ] (s : ) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
def QuotientAddGroup.rightRelDecidable.proof_1 {α : Type u_1} [inst : ] (s : ) (x : α) (y : α) :
Decidable (Setoid.r x y) = Decidable ((fun x y => y + -x s) x y)
Equations
instance QuotientGroup.rightRelDecidable {α : Type u_1} [inst : ] (s : ) [inst : DecidablePred fun x => x s] :
DecidableRel Setoid.r
Equations
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [inst : ] (s : ) (g : ) :
Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) (Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) g) = g
Equations
• One or more equations did not get rendered due to their size.
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [inst : ] (s : ) :
α s

Right cosets are in bijection with left cosets.

Equations
• One or more equations did not get rendered due to their size.
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_2 {α : Type u_1} [inst : ] (s : ) (a : α) (b : α) :
Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)
Equations
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_1 {α : Type u_1} [inst : ] (s : ) (a : α) (b : α) :
Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)
Equations
def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [inst : ] (s : ) (g : α s) :
Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) (Quotient.map' (fun g => -g) (_ : ∀ (a b : α), Setoid.r a bSetoid.r ((fun g => -g) a) ((fun g => -g) b)) g) = g
Equations
• One or more equations did not get rendered due to their size.
def QuotientGroup.quotientRightRelEquivQuotientLeftRel {α : Type u_1} [inst : ] (s : ) :
α s

Right cosets are in bijection with left cosets.

Equations
• One or more equations did not get rendered due to their size.
instance QuotientAddGroup.fintypeQuotientRightRel {α : Type u_1} [inst : ] (s : ) [inst : Fintype (α s)] :
Equations
instance QuotientGroup.fintypeQuotientRightRel {α : Type u_1} [inst : ] (s : ) [inst : Fintype (α s)] :
Equations
theorem QuotientAddGroup.card_quotient_rightRel {α : Type u_1} [inst : ] (s : ) [inst : Fintype (α s)] :
theorem QuotientGroup.card_quotient_rightRel {α : Type u_1} [inst : ] (s : ) [inst : Fintype (α s)] :
instance QuotientAddGroup.fintype {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : DecidableRel Setoid.r] :
Fintype (α s)
Equations
instance QuotientGroup.fintype {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : DecidableRel Setoid.r] :
Fintype (α s)
Equations
abbrev QuotientAddGroup.mk {α : Type u_1} [inst : ] {s : } (a : α) :
α s

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

Equations
• a =
@[inline]
abbrev QuotientGroup.mk {α : Type u_1} [inst : ] {s : } (a : α) :
α s

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

Equations
• a =
theorem QuotientAddGroup.mk_surjective {α : Type u_1} [inst : ] {s : } :
theorem QuotientGroup.mk_surjective {α : Type u_1} [inst : ] {s : } :
Function.Surjective QuotientGroup.mk
theorem QuotientAddGroup.induction_on {α : Type u_1} [inst : ] {s : } {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
theorem QuotientGroup.induction_on {α : Type u_1} [inst : ] {s : } {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
Equations
instance QuotientGroup.instCoeTCQuotientSubgroupInstHasQuotientSubgroup {α : Type u_1} [inst : ] {s : } :
CoeTC α (α s)
Equations
• QuotientGroup.instCoeTCQuotientSubgroupInstHasQuotientSubgroup = { coe := QuotientGroup.mk }
theorem QuotientAddGroup.induction_on' {α : Type u_1} [inst : ] {s : } {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
theorem QuotientGroup.induction_on' {α : Type u_1} [inst : ] {s : } {C : α sProp} (x : α s) (H : (z : α) → C z) :
C x
@[simp]
theorem QuotientAddGroup.quotient_liftOn_mk {α : Type u_2} [inst : ] {s : } {β : Sort u_1} (f : αβ) (h : ∀ (a b : α), Setoid.r a bf a = f b) (x : α) :
Quotient.liftOn' (x) f h = f x
@[simp]
theorem QuotientGroup.quotient_liftOn_mk {α : Type u_2} [inst : ] {s : } {β : Sort u_1} (f : αβ) (h : ∀ (a b : α), Setoid.r a bf a = f b) (x : α) :
Quotient.liftOn' (x) f h = f x
theorem QuotientAddGroup.forall_mk {α : Type u_1} [inst : ] {s : } {C : α sProp} :
((x : α s) → C x) (x : α) → C x
theorem QuotientGroup.forall_mk {α : Type u_1} [inst : ] {s : } {C : α sProp} :
((x : α s) → C x) (x : α) → C x
theorem QuotientAddGroup.exists_mk {α : Type u_1} [inst : ] {s : } {C : α sProp} :
(x, C x) x, C x
theorem QuotientGroup.exists_mk {α : Type u_1} [inst : ] {s : } {C : α sProp} :
(x, C x) x, C x
Equations
• = { default := 0 }
Equations
• = { default := 1 }
theorem QuotientAddGroup.eq {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
a = b a⁻¹ * b s
theorem QuotientAddGroup.eq' {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
a = b -a + b s
theorem QuotientGroup.eq' {α : Type u_1} [inst : ] {s : } {a : α} {b : α} :
a = b a⁻¹ * b s
theorem QuotientAddGroup.out_eq' {α : Type u_1} [inst : ] {s : } (a : α s) :
↑() = a
theorem QuotientGroup.out_eq' {α : Type u_1} [inst : ] {s : } (a : α s) :
↑() = a
theorem QuotientAddGroup.mk_out'_eq_mul {α : Type u_1} [inst : ] (s : ) (g : α) :
h, = g + h
theorem QuotientGroup.mk_out'_eq_mul {α : Type u_1} [inst : ] (s : ) (g : α) :
h, = g * h
@[simp]
theorem QuotientAddGroup.mk_add_of_mem {α : Type u_1} [inst : ] {s : } {b : α} (a : α) (hb : b s) :
↑(a + b) = a
@[simp]
theorem QuotientGroup.mk_mul_of_mem {α : Type u_1} [inst : ] {s : } {b : α} (a : α) (hb : b s) :
↑(a * b) = a
theorem QuotientAddGroup.eq_class_eq_leftCoset {α : Type u_1} [inst : ] (s : ) (g : α) :
{ x | x = g } = leftAddCoset g s
theorem QuotientGroup.eq_class_eq_leftCoset {α : Type u_1} [inst : ] (s : ) (g : α) :
{ x | x = g } = leftCoset g s
abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [inst : ] (N : ) (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
Equations
theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [inst : ] (N : ) (s : Set α) :
QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = Set.unionᵢ fun x => (fun y => y + x) ⁻¹' s
abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [inst : ] (N : ) (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
Equations
theorem QuotientGroup.preimage_image_mk {α : Type u_1} [inst : ] (N : ) (s : Set α) :
QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = Set.unionᵢ fun x => (fun y => y * x) ⁻¹' s
def AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [inst : ] {s : } (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
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [inst : ] {s : } (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
Equations
• One or more equations did not get rendered due to their size.
abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_2 {α : Type u_1} [inst : ] {s : } (motive : { x // x s }Prop) :
(x : { x // x s }) → ((g : α) → (hg : g s) → motive { val := g, property := hg }) → motive x
Equations
abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_1 {α : Type u_1} [inst : ] {s : } (g : α) (motive : ↑(leftAddCoset g s)Prop) :
(x : ↑(leftAddCoset g s)) → ((x : α) → (hx : x leftAddCoset g s) → motive { val := x, property := hx }) → motive x
Equations
def AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [inst : ] {s : } (g : α) (x : { x // x s }) :
a, a s (fun x => g + x) a = g + x
Equations
• (_ : a, a s (fun x => g + x) a = g + x) = (_ : a, a s (fun x => g + x) a = g + x)
def AddSubgroup.leftCosetEquivAddSubgroup.proof_1 {α : Type u_1} [inst : ] {s : } (g : α) (x : ↑(leftAddCoset g s)) :
-g + x s
Equations
def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [inst : ] {s : } (g : α) :
↑(leftAddCoset g s) { x // x s }

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

Equations
• One or more equations did not get rendered due to their size.
def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [inst : ] {s : } (g : α) :
↑(leftCoset g s) { x // x s }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [inst : ] {s : } (g : α) :
↑(rightAddCoset (s) g) { x // x s }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [inst : ] {s : } (g : α) (x : { x // x s }) :
a, a s (fun x => x + g) a = x + g
Equations
• (_ : a, a s (fun x => x + g) a = x + g) = (_ : a, a s (fun x => x + g) a = x + g)
abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [inst : ] {s : } (g : α) (motive : ↑(rightAddCoset (s) g)Prop) :
(x : ↑(rightAddCoset (s) g)) → ((x : α) → (hx : x rightAddCoset (s) g) → motive { val := x, property := hx }) → motive x
Equations
def AddSubgroup.rightCosetEquivAddSubgroup.proof_1 {α : Type u_1} [inst : ] {s : } (g : α) (x : ↑(rightAddCoset (s) g)) :
x + -g s
Equations
def AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [inst : ] {s : } (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
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [inst : ] {s : } (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
Equations
• One or more equations did not get rendered due to their size.
def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [inst : ] {s : } (g : α) :
↑(rightCoset (s) g) { x // x s }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_1 {α : Type u_1} [inst : ] {s : } (L : α s) :
({ x // x = L } ↑()) = ({ x // x = L } { x | x = ↑() })
Equations
• One or more equations did not get rendered due to their size.
noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [inst : ] {s : } :
α (α s) × { x // x s }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [inst : ] {s : } (L : α s) :
({ x // } { x // }) = ({ x // } { x // })
Equations
• One or more equations did not get rendered due to their size.
noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [inst : ] {s : } :
α (α s) × { x // x s }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) (q : α t) :
Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) (Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) q) = q
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) (q : α s) :
Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) (Quotient.map' id (_ : ∀ (_a _b : α), Setoid.r _a _bSetoid.r (id _a) (id _b)) q) = q
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) :
α s α t

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivOfEq.proof_2 {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
Setoid.r (id _a) (id _b)
Equations
def AddSubgroup.quotientEquivOfEq.proof_1 {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) (_a : α) (_b : α) (h' : Setoid.r _a _b) :
Setoid.r (id _a) (id _b)
Equations
def Subgroup.quotientEquivOfEq {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) :
α s α t

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

Equations
• One or more equations did not get rendered due to their size.
theorem Subgroup.quotientEquivOfEq_mk {α : Type u_1} [inst : ] {s : } {t : } (h : s = t) (a : α) :
↑() a = a
def AddSubgroup.quotientEquivSumOfLe'.proof_1 {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (b : α) (c : α) (h : Setoid.r b c) :
Setoid.r (id b) (id c)
Equations
def AddSubgroup.quotientEquivSumOfLe' {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) :
α s (α t) × { x // x t }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe'.proof_4 {α : Type u_1} [inst : ] {s : } {t : } (f : α tα) (a : (α t) × { x // x 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)
Equations
• (_ : Setoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)) = (_ : Setoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c))
def AddSubgroup.quotientEquivSumOfLe'.proof_6 {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (t : (α t) × { x // x t } ) :
(fun a => (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f () + g, property := (_ : -f () + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) b) ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) c)) a)) ((fun a => Quotient.map' (fun b => f a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => f a.fst + b) b) ((fun b => f a.fst + b) c)) a.snd) t) = t
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe'.proof_3 {α : Type u_1} [inst : ] {s : } {t : } (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 () + g, property := (_ : -f () + g t) }) b) ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) c)
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe'.proof_2 {α : Type u_1} [inst : ] {t : } (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (g : α) :
-f () + g t
Equations
def AddSubgroup.quotientEquivSumOfLe'.proof_5 {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (q : ) :
(fun a => Quotient.map' (fun b => f a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.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 cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f () + g, property := (_ : -f () + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) b) ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) c)) a)) q) = q
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe'_symm_apply {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : (α t) × { x // x t } ) :
↑(Equiv.symm ()) a = Quotient.map' (fun b => f a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.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} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : (α t) × { x // x t } ) :
↑(Equiv.symm ()) a = Quotient.map' (fun b => f a.fst * b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => f a.fst * b) b) ((fun b => f a.fst * b) c)) a.snd
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe'_apply {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α s) :
↑() a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := -f () + g, property := (_ : -f () + g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) b) ((fun g => { val := -f () + g, property := (_ : -f () + g t) }) c)) a)
@[simp]
theorem Subgroup.quotientEquivProdOfLe'_apply {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) (a : α s) :
↑() a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := (f ())⁻¹ * g, property := (_ : (f ())⁻¹ * g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := (f ())⁻¹ * g, property := (_ : (f ())⁻¹ * g t) }) b) ((fun g => { val := (f ())⁻¹ * g, property := (_ : (f ())⁻¹ * g t) }) c)) a)
def Subgroup.quotientEquivProdOfLe' {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (f : α tα) (hf : Function.RightInverse f QuotientGroup.mk) :
α s (α t) × { x // x t }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientEquivSumOfLe.proof_1 {α : Type u_1} [inst : ] {t : } (q : ) :
Equations
• (_ : ∀ (q : ), ) = (_ : ∀ (q : ), )
noncomputable def AddSubgroup.quotientEquivSumOfLe {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) :
α s (α t) × { x // x t }

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

Equations
@[simp]
theorem Subgroup.quotientEquivProdOfLe_symm_apply {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (a : (α t) × { x // x t } ) :
↑() a = Quotient.map' (fun b => Quotient.out' a.fst * b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.r ((fun b => Quotient.out' a.fst * b) b) ((fun b => Quotient.out' a.fst * b) c)) a.snd
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe_symm_apply {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (a : (α t) × { x // x t } ) :
↑() a = Quotient.map' (fun b => Quotient.out' a.fst + b) (_ : ∀ (b c : { x // x t }), Setoid.r b cSetoid.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} [inst : ] {s : } {t : } (h_le : s t) (a : α s) :
↑() a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := ()⁻¹ * g, property := (_ : ()⁻¹ * g t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := ()⁻¹ * g, property := (_ : ()⁻¹ * g t) }) b) ((fun g => { val := ()⁻¹ * g, property := (_ : ()⁻¹ * g t) }) c)) a)
@[simp]
theorem AddSubgroup.quotientEquivSumOfLe_apply {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) (a : α s) :
↑() a = (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b cSetoid.r (id b) (id c)) a, Quotient.map' (fun g => { val := , property := (_ : t) }) (_ : ∀ (b c : α), Setoid.r b cSetoid.r ((fun g => { val := , property := (_ : t) }) b) ((fun g => { val := , property := (_ : t) }) c)) a)
noncomputable def Subgroup.quotientEquivProdOfLe {α : Type u_1} [inst : ] {s : } {t : } (h_le : s t) :
α s (α t) × { x // x t }

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

Equations
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe.proof_1 {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (a : { x // x s }) (b : { x // x s }) :
Setoid.r a bSetoid.r (↑() a) (↑() b)
Equations
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) :
{ x // x s } { x // x t }

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe.proof_2 {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (q₁ : ) (q₂ : ) :
Quotient.map' (_ : ∀ (a b : { x // x s }), Setoid.r a bSetoid.r (↑() a) (↑() b)) q₁ = Quotient.map' (_ : ∀ (a b : { x // x s }), Setoid.r a bSetoid.r (↑() a) (↑() b)) q₂q₁ = q₂
Equations
• One or more equations did not get rendered due to their size.
def Subgroup.quotientSubgroupOfEmbeddingOfLe {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) :
{ x // x s } { x // x t }

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe_apply_mk {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (g : { x // x s }) :
= ↑(↑() g)
@[simp]
theorem Subgroup.quotientSubgroupOfEmbeddingOfLe_apply_mk {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (g : { x // x s }) :
= ↑(↑() g)
def AddSubgroup.quotientAddSubgroupOfMapOfLe.proof_1 {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (a : { x // x H }) (b : { x // x H }) :
Setoid.r a bSetoid.r (id a) (id b)
Equations
def AddSubgroup.quotientAddSubgroupOfMapOfLe {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) :
{ x // x H } { x // x H }

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

Equations
def Subgroup.quotientSubgroupOfMapOfLe {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) :
{ x // x H } { x // x H }

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

Equations
@[simp]
theorem AddSubgroup.quotientAddSubgroupOfMapOfLe_apply_mk {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (g : { x // x H }) :
@[simp]
theorem Subgroup.quotientSubgroupOfMapOfLe_apply_mk {α : Type u_1} [inst : ] {s : } {t : } (H : ) (h : s t) (g : { x // x H }) :
= g
def AddSubgroup.quotientMapOfLe.proof_1 {α : Type u_1} [inst : ] {s : } {t : } (h : s t) (a : α) (b : α) :
Setoid.r a bSetoid.r (id a) (id b)
Equations
def AddSubgroup.quotientMapOfLe {α : Type u_1} [inst : ] {s : } {t : } (h : s t) :
α sα t

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

Equations
def Subgroup.quotientMapOfLe {α : Type u_1} [inst : ] {s : } {t : } (h : s t) :
α sα t

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

Equations
@[simp]
theorem AddSubgroup.quotientMapOfLe_apply_mk {α : Type u_1} [inst : ] {s : } {t : } (h : s t) (g : α) :
= g
@[simp]
theorem Subgroup.quotientMapOfLe_apply_mk {α : Type u_1} [inst : ] {s : } {t : } (h : s t) (g : α) :
= g
def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (i : ι) :
infᵢ f f i
Equations
def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (H : ) (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 (_ : infᵢ f f i) q) q₁ = (fun q i => AddSubgroup.quotientAddSubgroupOfMapOfLe H (_ : infᵢ f f i) q) q₂q₁ = q₂
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (H : ) :
{ x // x H } AddSubgroup.addSubgroupOf (i, f i) H (i : ι) → { x // x H }

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (H : ) (q : { x // x H } Subgroup.subgroupOf (i, f i) H) (i : ι) :
@[simp]
theorem AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding_apply {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (H : ) (q : { x // x H } AddSubgroup.addSubgroupOf (i, f i) H) (i : ι) :
def Subgroup.quotientInfᵢSubgroupOfEmbedding {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (H : ) :
{ 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⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H↪ Π i, H ⧸ (f i).subgroupOf H⧸ (f i).subgroupOf H.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding_apply_mk {α : Type u_2} [inst : ] {ι : Type u_1} (f : ι) (H : ) (g : { x // x H }) (i : ι) :
↑() (g) i = g
@[simp]
theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply_mk {α : Type u_2} [inst : ] {ι : Type u_1} (f : ι) (H : ) (g : { x // x H }) (i : ι) :
↑() (g) i = g
def AddSubgroup.quotientInfᵢEmbedding.proof_2 {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (q₁ : Quotient (QuotientAddGroup.leftRel (i, f i))) (q₂ : Quotient (QuotientAddGroup.leftRel (i, f i))) :
(fun q i => AddSubgroup.quotientMapOfLe (_ : infᵢ f f i) q) q₁ = (fun q i => AddSubgroup.quotientMapOfLe (_ : infᵢ f f i) q) q₂q₁ = q₂
Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.quotientInfᵢEmbedding.proof_1 {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (i : ι) :
infᵢ f f i
Equations
def AddSubgroup.quotientInfᵢEmbedding {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) :
(α i, f i) (i : ι) → α f i

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientInfᵢEmbedding_apply {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (q : α i, f i) (i : ι) :
@[simp]
theorem Subgroup.quotientInfᵢEmbedding_apply {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) (q : α i, f i) (i : ι) :
def Subgroup.quotientInfᵢEmbedding {α : Type u_1} [inst : ] {ι : Type u_2} (f : ι) :
(α i, f i) (i : ι) → α f i

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.quotientInfᵢEmbedding_apply_mk {α : Type u_2} [inst : ] {ι : Type u_1} (f : ι) (g : α) (i : ι) :
↑() (g) i = g
@[simp]
theorem Subgroup.quotientInfᵢEmbedding_apply_mk {α : Type u_2} [inst : ] {ι : Type u_1} (f : ι) (g : α) (i : ι) :
↑() (g) i = g
theorem AddSubgroup.card_eq_card_quotient_add_card_addSubgroup {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : Fintype { x // x s }] [inst : DecidablePred fun a => a s] :
= Fintype.card (α s) * Fintype.card { x // x s }
theorem Subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : Fintype { x // x s }] [inst : DecidablePred fun a => a s] :
= Fintype.card (α s) * Fintype.card { x // x s }
theorem AddSubgroup.card_addSubgroup_dvd_card {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : Fintype { x // x s }] :
Fintype.card { x // x s }

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} [inst : ] [inst : ] (s : ) [inst : Fintype { x // x s }] :
Fintype.card { x // x s }

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

theorem AddSubgroup.card_quotient_dvd_card {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : DecidablePred fun x => x s] :
theorem Subgroup.card_quotient_dvd_card {α : Type u_1} [inst : ] [inst : ] (s : ) [inst : DecidablePred fun x => x s] :
theorem AddSubgroup.card_dvd_of_injective {α : Type u_1} [inst : ] {H : Type u_2} [inst : ] [inst : ] [inst : ] (f : α →+ H) (hf : ) :
theorem Subgroup.card_dvd_of_injective {α : Type u_1} [inst : ] {H : Type u_2} [inst : ] [inst : ] [inst : ] (f : α →* H) (hf : ) :
theorem AddSubgroup.card_dvd_of_le {α : Type u_1} [inst : ] {H : } {K : } [inst : Fintype { x // x H }] [inst : 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} [inst : ] {H : } {K : } [inst : Fintype { x // x H }] [inst : 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_2} [inst : ] {H : Type u_1} [inst : ] (K : ) [inst : Fintype { x // x K }] (f : α →+ H) [inst : Fintype { x // x }] (hf : ) :
Fintype.card { x // x } Fintype.card { x // x K }
theorem Subgroup.card_comap_dvd_of_injective {α : Type u_2} [inst : ] {H : Type u_1} [inst : ] (K : ) [inst : Fintype { x // x K }] (f : α →* H) [inst : Fintype { x // x }] (hf : ) :
Fintype.card { x // x } Fintype.card { x // x K }
abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [inst : ] (s : ) (t : Set (α s)) (motive : { x // x s } × tProp) :
(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
Equations
• One or more equations did not get rendered due to their size.
noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [inst : ] (s : ) (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⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t× t.

Equations
• One or more equations did not get rendered due to their size.
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [inst : ] (s : ) (t : Set (α s)) :
∀ (x : { x // x s } × t), (fun a => ({ val := - + a, property := (_ : - + 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
Equations
• One or more equations did not get rendered due to their size.
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [inst : ] (s : ) (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 := - + a, property := (_ : - + a s) }, { val := a, property := (_ : a QuotientAddGroup.mk ⁻¹' t) })) x) = x
Equations
• One or more equations did not get rendered due to their size.
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_1 {α : Type u_1} [inst : ] (s : ) (t : Set (α s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) :
- + a s
Equations
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_3 {α : Type u_1} [inst : ] (s : ) (t : Set (α s)) (a : { x // x s } × t) :
↑(Quotient.out' a.snd + a.fst) t
Equations
def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_2 {α : Type u_1} [inst : ] (s : ) (t : Set (α s)) (a : ↑(QuotientAddGroup.mk ⁻¹' t)) :
a QuotientAddGroup.mk ⁻¹' t
Equations
abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [inst : ] (s : ) (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
Equations
noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [inst : ] (s : ) (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⧸ s, then there is a (typically non-canonical) bijection between the preimage of t in α and the product s × t× t.

Equations
• One or more equations did not get rendered due to their size.