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

ink

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

• leftAddCoset a s = (fun x => a + x) '' s

ink

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

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

ink

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

• rightAddCoset s a = (fun x => x + a) '' s

ink

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

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

ink

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

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

Equations

• Coset.«term_*l_» = Lean.ParserDescr.trailingNode `Coset.term_*l_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *l ") (Lean.ParserDescr.cat `term 71))

ink

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

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

Equations

• Coset.«term_+l_» = Lean.ParserDescr.trailingNode `Coset.term_+l_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +l ") (Lean.ParserDescr.cat `term 71))

ink

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

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

Equations

• Coset.«term_*r_» = Lean.ParserDescr.trailingNode `Coset.term_*r_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *r ") (Lean.ParserDescr.cat `term 71))

ink

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

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

Equations

• Coset.«term_+r_» = Lean.ParserDescr.trailingNode `Coset.term_+r_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +r ") (Lean.ParserDescr.cat `term 71))

ink

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

ink

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

ink

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

ink

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

ink

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

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

Equations

• LeftAddCosetEquivalence s a b = (leftAddCoset a s = leftAddCoset b s)

ink

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

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

Equations

• LeftCosetEquivalence s a b = (leftCoset a s = leftCoset b s)

ink

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

ink

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

ink

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

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

Equations

• RightAddCosetEquivalence s a b = (rightAddCoset s a = rightAddCoset s b)

ink

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

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

Equations

• RightCosetEquivalence s a b = (rightCoset s a = rightCoset s b)

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

abbrev mem_leftAddCoset_iff.match_1 {α : Type u_1} [inst : 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

Equations

• mem_leftAddCoset_iff.match_1 a motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

ink

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

ink

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

ink

abbrev mem_rightAddCoset_iff.match_1 {α : Type u_1} [inst : 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

Equations

• mem_rightAddCoset_iff.match_1 a motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

abbrev orbit_addSubgroup_eq_rightCoset.match_2 {α : Type u_1} [inst : 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

Equations

• orbit_addSubgroup_eq_rightCoset.match_2 s a _b motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

ink

abbrev orbit_addSubgroup_eq_rightCoset.match_1 {α : Type u_1} [inst : 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 x => x +ᵥ a) c = _b) → motive (_ : ∃ y, (fun x => x +ᵥ a) y = _b)) → motive x

Equations

• orbit_addSubgroup_eq_rightCoset.match_1 s a _b motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

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

Equations

• QuotientAddGroup.leftRel s = AddAction.orbitRel { x // x ∈ ↑AddSubgroup.opposite s } α

ink

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

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

Equations

• QuotientGroup.leftRel s = MulAction.orbitRel { x // x ∈ ↑Subgroup.opposite s } α

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

• (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => -x + y ∈ s) x y)) = (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => -x + y ∈ s) x y))

ink

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

Equations

• QuotientAddGroup.leftRelDecidable s x y = Eq.mpr (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => -x + y ∈ s) x y)) (inst (-x + y))

ink

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

Equations

• QuotientGroup.leftRelDecidable s x y = Eq.mpr (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => x⁻¹ * y ∈ s) x y)) (inst (x⁻¹ * y))

ink

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

α ⧸ 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 => Quotient (QuotientAddGroup.leftRel s) }

ink

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

α ⧸ 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 => Quotient (QuotientGroup.leftRel s) }

ink

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

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

Equations

• QuotientAddGroup.rightRel s = AddAction.orbitRel { x // x ∈ s } α

ink

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

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

Equations

• QuotientGroup.rightRel s = MulAction.orbitRel { x // x ∈ s } α

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

• QuotientAddGroup.rightRelDecidable s x y = Eq.mpr (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => y + -x ∈ s) x y)) (inst (y + -x))

ink

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

Equations

• (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => y + -x ∈ s) x y)) = (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => y + -x ∈ s) x y))

ink

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

Equations

• QuotientGroup.rightRelDecidable s x y = Eq.mpr (_ : Decidable (Setoid.r x y) = Decidable ((fun x y => y * x⁻¹ ∈ s) x y)) (inst (y * x⁻¹))

ink

def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_3 {α : Type u_1} [inst : 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

Equations

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

ink

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

Right cosets are in bijection with left cosets.

Equations

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

ink

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

Equations

• (_ : Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)) = (_ : Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b))

ink

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

Equations

• (_ : Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b)) = (_ : Setoid.r a b → Setoid.r ((fun g => -g) a) ((fun g => -g) b))

ink

def QuotientAddGroup.quotientRightRelEquivQuotientLeftRel.proof_4 {α : Type u_1} [inst : 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

Equations

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

ink

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

Right cosets are in bijection with left cosets.

Equations

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

ink

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

Equations

• QuotientAddGroup.fintypeQuotientRightRel s = Fintype.ofEquiv (α ⧸ s) (Equiv.symm (QuotientAddGroup.quotientRightRelEquivQuotientLeftRel s))

ink

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

Equations

• QuotientGroup.fintypeQuotientRightRel s = Fintype.ofEquiv (α ⧸ s) (Equiv.symm (QuotientGroup.quotientRightRelEquivQuotientLeftRel s))

ink

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

ink

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

ink

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

Equations

• QuotientAddGroup.fintype s = Quotient.fintype (QuotientAddGroup.leftRel s)

ink

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

Equations

• QuotientGroup.fintype s = Quotient.fintype (QuotientGroup.leftRel s)

ink

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

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

Equations

• ↑a = Quotient.mk'' a

ink

@[inline]

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

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

Equations

• ↑a = Quotient.mk'' a

ink

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

ink

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

ink

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

ink

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

ink

instance QuotientAddGroup.instCoeTCQuotientAddSubgroupInstHasQuotientAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} : CoeTC α (α ⧸ s)

Equations

• QuotientAddGroup.instCoeTCQuotientAddSubgroupInstHasQuotientAddSubgroup = { coe := QuotientAddGroup.mk }

ink

instance QuotientGroup.instCoeTCQuotientSubgroupInstHasQuotientSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} : CoeTC α (α ⧸ s)

Equations

• QuotientGroup.instCoeTCQuotientSubgroupInstHasQuotientSubgroup = { coe := QuotientGroup.mk }

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

• QuotientAddGroup.instInhabitedQuotientAddSubgroupInstHasQuotientAddSubgroup s = { default := ↑0 }

ink

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

Equations

• QuotientGroup.instInhabitedQuotientSubgroupInstHasQuotientSubgroup s = { default := ↑1 }

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

abbrev QuotientAddGroup.preimage_image_mk.match_1 {α : Type u_1} [inst : 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

Equations

• QuotientAddGroup.preimage_image_mk.match_1 N s x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

ink

theorem QuotientAddGroup.preimage_image_mk {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α) : QuotientAddGroup.mk ⁻¹' (QuotientAddGroup.mk '' s) = Set.unionᵢ fun x => (fun y => y + ↑x) ⁻¹' s

ink

abbrev QuotientAddGroup.preimage_image_mk.match_2 {α : Type u_1} [inst : 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

Equations

• QuotientAddGroup.preimage_image_mk.match_2 N s x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

ink

theorem QuotientGroup.preimage_image_mk {α : Type u_1} [inst : Group α] (N : Subgroup α) (s : Set α) : QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = Set.unionᵢ fun x => (fun y => y * ↑x) ⁻¹' s

ink

def AddSubgroup.leftCosetEquivAddSubgroup.proof_4 {α : Type u_1} [inst : 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

Equations

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

ink

def AddSubgroup.leftCosetEquivAddSubgroup.proof_3 {α : Type u_1} [inst : 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

Equations

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

ink

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

Equations

• AddSubgroup.leftCosetEquivAddSubgroup.match_2 motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

ink

abbrev AddSubgroup.leftCosetEquivAddSubgroup.match_1 {α : Type u_1} [inst : 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

Equations

• AddSubgroup.leftCosetEquivAddSubgroup.match_1 g motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

ink

def AddSubgroup.leftCosetEquivAddSubgroup.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (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)

ink

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

Equations

• (_ : -g + ↑x ∈ ↑s) = (_ : -g + ↑x ∈ ↑s)

ink

def AddSubgroup.leftCosetEquivAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (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.

ink

def Subgroup.leftCosetEquivSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} (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.

ink

def AddSubgroup.rightCosetEquivAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (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.

ink

def AddSubgroup.rightCosetEquivAddSubgroup.proof_2 {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (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)

ink

abbrev AddSubgroup.rightCosetEquivAddSubgroup.match_1 {α : Type u_1} [inst : 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

Equations

• AddSubgroup.rightCosetEquivAddSubgroup.match_1 g motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

ink

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

Equations

• (_ : ↑x + -g ∈ ↑s) = (_ : ↑x + -g ∈ ↑s)

ink

def AddSubgroup.rightCosetEquivAddSubgroup.proof_3 {α : Type u_1} [inst : 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

Equations

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

ink

def AddSubgroup.rightCosetEquivAddSubgroup.proof_4 {α : Type u_1} [inst : 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

Equations

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

ink

def Subgroup.rightCosetEquivSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} (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.

ink

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

Equations

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

ink

noncomputable def AddSubgroup.addGroupEquivQuotientProdAddSubgroup {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} : α ≃ (α ⧸ 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.

ink

def AddSubgroup.addGroupEquivQuotientProdAddSubgroup.proof_2 {α : Type u_1} [inst : 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 })

Equations

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

ink

noncomputable def Subgroup.groupEquivQuotientProdSubgroup {α : Type u_1} [inst : Group α] {s : Subgroup α} : α ≃ (α ⧸ 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.

ink

def AddSubgroup.quotientEquivOfEq.proof_4 {α : Type u_1} [inst : 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

Equations

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

ink

def AddSubgroup.quotientEquivOfEq.proof_3 {α : Type u_1} [inst : 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

Equations

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

ink

def AddSubgroup.quotientEquivOfEq {α : Type u_1} [inst : 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.

Equations

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

ink

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

Equations

• (_ : Setoid.r (id _a) (id _b)) = (_ : Setoid.r (id _a) (id _b))

ink

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

Equations

• (_ : Setoid.r (id _a) (id _b)) = (_ : Setoid.r (id _a) (id _b))

ink

def Subgroup.quotientEquivOfEq {α : Type u_1} [inst : 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.

Equations

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

ink

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

ink

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

Equations

• (_ : Setoid.r (id b) (id c)) = (_ : Setoid.r (id b) (id c))

ink

def AddSubgroup.quotientEquivSumOfLe' {α : Type u_1} [inst : 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≤ 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.

ink

def AddSubgroup.quotientEquivSumOfLe'.proof_4 {α : Type u_1} [inst : 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)

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))

ink

def AddSubgroup.quotientEquivSumOfLe'.proof_6 {α : Type u_1} [inst : 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

Equations

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

ink

def AddSubgroup.quotientEquivSumOfLe'.proof_3 {α : Type u_1} [inst : 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)

Equations

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

ink

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

Equations

• (_ : -f (Quotient.mk'' g) + g ∈ t) = (_ : -f (Quotient.mk'' g) + g ∈ t)

ink

def AddSubgroup.quotientEquivSumOfLe'.proof_5 {α : Type u_1} [inst : 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

Equations

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

ink

@[simp]

theorem AddSubgroup.quotientEquivSumOfLe'_symm_apply {α : Type u_1} [inst : 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) : ↑(Equiv.symm (AddSubgroup.quotientEquivSumOfLe' h_le f hf)) 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

ink

@[simp]

theorem Subgroup.quotientEquivProdOfLe'_symm_apply {α : Type u_1} [inst : 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) : ↑(Equiv.symm (Subgroup.quotientEquivProdOfLe' h_le f hf)) 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

ink

@[simp]

theorem AddSubgroup.quotientEquivSumOfLe'_apply {α : Type u_1} [inst : 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)

ink

@[simp]

theorem Subgroup.quotientEquivProdOfLe'_apply {α : Type u_1} [inst : 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)

ink

def Subgroup.quotientEquivProdOfLe' {α : Type u_1} [inst : 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≤ 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.

ink

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

Equations

• (_ : ∀ (q : Quotient (QuotientAddGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q) = (_ : ∀ (q : Quotient (QuotientAddGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q)

ink

noncomputable def AddSubgroup.quotientEquivSumOfLe {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s 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

• AddSubgroup.quotientEquivSumOfLe h_le = AddSubgroup.quotientEquivSumOfLe' h_le Quotient.out' (_ : ∀ (q : Quotient (QuotientAddGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q)

ink

@[simp]

theorem Subgroup.quotientEquivProdOfLe_symm_apply {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × { x // x ∈ t } ⧸ Subgroup.subgroupOf s t) : ↑(Equiv.symm (Subgroup.quotientEquivProdOfLe h_le)) 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

ink

@[simp]

theorem AddSubgroup.quotientEquivSumOfLe_symm_apply {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {t : AddSubgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × { x // x ∈ t } ⧸ AddSubgroup.addSubgroupOf s t) : ↑(Equiv.symm (AddSubgroup.quotientEquivSumOfLe h_le)) 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

ink

@[simp]

theorem Subgroup.quotientEquivProdOfLe_apply {α : Type u_1} [inst : 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)

ink

@[simp]

theorem AddSubgroup.quotientEquivSumOfLe_apply {α : Type u_1} [inst : 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)

ink

noncomputable def Subgroup.quotientEquivProdOfLe {α : Type u_1} [inst : Group α] {s : Subgroup α} {t : Subgroup α} (h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × { x // x ∈ t } ⧸ Subgroup.subgroupOf s 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

• Subgroup.quotientEquivProdOfLe h_le = Subgroup.quotientEquivProdOfLe' h_le Quotient.out' (_ : ∀ (q : Quotient (QuotientGroup.leftRel t)), Quotient.mk'' (Quotient.out' q) = q)

ink

def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe.proof_1 {α : Type u_1} [inst : 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)

Equations

• (_ : Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b)) = (_ : Setoid.r a b → Setoid.r (↑(AddSubgroup.inclusion h) a) (↑(AddSubgroup.inclusion h) b))

ink

def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe {α : Type u_1} [inst : 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≤ 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.

ink

def AddSubgroup.quotientAddSubgroupOfEmbeddingOfLe.proof_2 {α : Type u_1} [inst : 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₂

Equations

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

ink

def Subgroup.quotientSubgroupOfEmbeddingOfLe {α : Type u_1} [inst : 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≤ 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.

ink

@[simp]

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

ink

@[simp]

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

ink

def AddSubgroup.quotientAddSubgroupOfMapOfLe.proof_1 {α : Type u_1} [inst : 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)

Equations

• (_ : Setoid.r a b → Setoid.r (id a) (id b)) = (_ : Setoid.r a b → Setoid.r (id a) (id b))

ink

def AddSubgroup.quotientAddSubgroupOfMapOfLe {α : Type u_1} [inst : 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≤ 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

• AddSubgroup.quotientAddSubgroupOfMapOfLe H h = Quotient.map' id (_ : ∀ (a b : { x // x ∈ H }), Setoid.r a b → Setoid.r (id a) (id b))

ink

def Subgroup.quotientSubgroupOfMapOfLe {α : Type u_1} [inst : 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≤ 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

• Subgroup.quotientSubgroupOfMapOfLe H h = Quotient.map' id (_ : ∀ (a b : { x // x ∈ H }), Setoid.r a b → Setoid.r (id a) (id b))

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• (_ : Setoid.r a b → Setoid.r (id a) (id b)) = (_ : Setoid.r a b → Setoid.r (id a) (id b))

ink

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

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

Equations

• AddSubgroup.quotientMapOfLe h = Quotient.map' id (_ : ∀ (a b : α), Setoid.r a b → Setoid.r (id a) (id b))

ink

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

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

Equations

• Subgroup.quotientMapOfLe h = Quotient.map' id (_ : ∀ (a b : α), Setoid.r a b → Setoid.r (id a) (id b))

ink

@[simp]

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

ink

@[simp]

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

ink

def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding.proof_1 {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (i : ι) : infᵢ f ≤ f i

Equations

• (_ : infᵢ f ≤ f i) = (_ : infᵢ f ≤ f i)

ink

def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding.proof_2 {α : Type u_1} [inst : 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 (_ : 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.

ink

def AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding {α : Type u_1} [inst : 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⧸ (⨅ 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.

ink

@[simp]

theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) (q : { x // x ∈ H } ⧸ Subgroup.subgroupOf (⨅ i, f i) H) (i : ι) : ↑(Subgroup.quotientInfᵢSubgroupOfEmbedding f H) q i = Subgroup.quotientSubgroupOfMapOfLe H (_ : infᵢ f ≤ f i) q

ink

@[simp]

theorem AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding_apply {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (H : AddSubgroup α) (q : { x // x ∈ H } ⧸ AddSubgroup.addSubgroupOf (⨅ i, f i) H) (i : ι) : ↑(AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding f H) q i = AddSubgroup.quotientAddSubgroupOfMapOfLe H (_ : infᵢ f ≤ f i) q

ink

def Subgroup.quotientInfᵢSubgroupOfEmbedding {α : Type u_1} [inst : 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⧸ (⨅ 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.

ink

@[simp]

theorem AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding_apply_mk {α : Type u_2} [inst : AddGroup α] {ι : Type u_1} (f : ι → AddSubgroup α) (H : AddSubgroup α) (g : { x // x ∈ H }) (i : ι) : ↑(AddSubgroup.quotientInfᵢAddSubgroupOfEmbedding f H) (↑g) i = ↑g

ink

@[simp]

theorem Subgroup.quotientInfᵢSubgroupOfEmbedding_apply_mk {α : Type u_2} [inst : Group α] {ι : Type u_1} (f : ι → Subgroup α) (H : Subgroup α) (g : { x // x ∈ H }) (i : ι) : ↑(Subgroup.quotientInfᵢSubgroupOfEmbedding f H) (↑g) i = ↑g

ink

def AddSubgroup.quotientInfᵢEmbedding.proof_2 {α : Type u_1} [inst : 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 (_ : 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.

ink

def AddSubgroup.quotientInfᵢEmbedding.proof_1 {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (i : ι) : infᵢ f ≤ f i

Equations

• (_ : infᵢ f ≤ f i) = (_ : infᵢ f ≤ f i)

ink

def AddSubgroup.quotientInfᵢEmbedding {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) : (α ⧸ ⨅ 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.

ink

@[simp]

theorem AddSubgroup.quotientInfᵢEmbedding_apply {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α) (q : α ⧸ ⨅ i, f i) (i : ι) : ↑(AddSubgroup.quotientInfᵢEmbedding f) q i = AddSubgroup.quotientMapOfLe (_ : infᵢ f ≤ f i) q

ink

@[simp]

theorem Subgroup.quotientInfᵢEmbedding_apply {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (q : α ⧸ ⨅ i, f i) (i : ι) : ↑(Subgroup.quotientInfᵢEmbedding f) q i = Subgroup.quotientMapOfLe (_ : infᵢ f ≤ f i) q

ink

def Subgroup.quotientInfᵢEmbedding {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) : (α ⧸ ⨅ 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.

ink

@[simp]

theorem AddSubgroup.quotientInfᵢEmbedding_apply_mk {α : Type u_2} [inst : AddGroup α] {ι : Type u_1} (f : ι → AddSubgroup α) (g : α) (i : ι) : ↑(AddSubgroup.quotientInfᵢEmbedding f) (↑g) i = ↑g

ink

@[simp]

theorem Subgroup.quotientInfᵢEmbedding_apply_mk {α : Type u_2} [inst : Group α] {ι : Type u_1} (f : ι → Subgroup α) (g : α) (i : ι) : ↑(Subgroup.quotientInfᵢEmbedding f) (↑g) i = ↑g

ink

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

ink

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

ink

theorem AddSubgroup.card_addSubgroup_dvd_card {α : Type u_1} [inst : AddGroup α] [inst : Fintype α] (s : AddSubgroup α) [inst : 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.

ink

theorem Subgroup.card_subgroup_dvd_card {α : Type u_1} [inst : Group α] [inst : Fintype α] (s : Subgroup α) [inst : 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.

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_2 {α : Type u_1} [inst : 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

Equations

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

ink

noncomputable def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet {α : Type u_1} [inst : 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⧸ 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.

ink

def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_5 {α : Type u_1} [inst : 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

Equations

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

ink

def QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.proof_4 {α : Type u_1} [inst : 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

Equations

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

ink

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

Equations

• (_ : -Quotient.out' ↑↑a + ↑a ∈ s) = (_ : -Quotient.out' ↑↑a + ↑a ∈ s)

ink

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

Equations

• (_ : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t) = (_ : ↑(Quotient.out' ↑a.snd + ↑a.fst) ∈ t)

ink

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

Equations

• (_ : ↑a ∈ QuotientAddGroup.mk ⁻¹' t) = (_ : ↑a ∈ QuotientAddGroup.mk ⁻¹' t)

ink

abbrev QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 {α : Type u_1} [inst : 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

Equations

• QuotientAddGroup.preimageMkEquivAddSubgroupProdSet.match_1 s t motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

ink

noncomputable def QuotientGroup.preimageMkEquivSubgroupProdSet {α : Type u_1} [inst : 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⧸ 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.