# mathlib3documentation

group_theory.coset

# Cosets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

• `left_coset a s`: the left coset `a * s` for an element `a : α` and a subset `s ⊆ α`, for an `add_group` this is `left_add_coset a s`.
• `right_coset s a`: the right coset `s * a` for an element `a : α` and a subset `s ⊆ α`, for an `add_group` this is `right_add_coset s a`.
• `quotient_group.quotient s`: the quotient type representing the left cosets with respect to a subgroup `s`, for an `add_group` this is `quotient_add_group.quotient s`.
• `quotient_group.mk`: the canonical map from `α` to `α/s` for a subgroup `s` of `α`, for an `add_group` this is `quotient_add_group.mk`.
• `subgroup.left_coset_equiv_subgroup`: the natural bijection between a left coset and the subgroup, for an `add_group` this is `add_subgroup.left_coset_equiv_add_subgroup`.

## Notation #

• `a *l s`: for `left_coset a s`.

• `a +l s`: for `left_add_coset a s`.

• `s *r a`: for `right_coset s a`.

• `s +r a`: for `right_add_coset s a`.

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

def left_add_coset {α : Type u_1} [has_add α] (a : α) (s : set α) :
set α

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

Equations
• = (λ (x : α), a + x) '' s
def left_coset {α : Type u_1} [has_mul α] (a : α) (s : set α) :
set α

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

Equations
• s = (λ (x : α), a * x) '' s
def right_coset {α : Type u_1} [has_mul α] (s : set α) (a : α) :
set α

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

Equations
• a = (λ (x : α), x * a) '' s
def right_add_coset {α : Type u_1} [has_add α] (s : set α) (a : α) :
set α

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

Equations
• = (λ (x : α), x + a) '' s
theorem mem_left_coset {α : Type u_1} [has_mul α] {s : set α} {x : α} (a : α) (hxS : x s) :
a * x s
theorem mem_left_add_coset {α : Type u_1} [has_add α] {s : set α} {x : α} (a : α) (hxS : x s) :
a + x
theorem mem_right_coset {α : Type u_1} [has_mul α] {s : set α} {x : α} (a : α) (hxS : x s) :
x * a a
theorem mem_right_add_coset {α : Type u_1} [has_add α] {s : set α} {x : α} (a : α) (hxS : x s) :
x + a
def left_coset_equivalence {α : Type u_1} [has_mul α] (s : set α) (a b : α) :
Prop

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

Equations
• = s = s)
def left_add_coset_equivalence {α : Type u_1} [has_add α] (s : set α) (a b : α) :
Prop

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

Equations
• = s = s)
theorem left_add_coset_equivalence_rel {α : Type u_1} [has_add α] (s : set α) :
theorem left_coset_equivalence_rel {α : Type u_1} [has_mul α] (s : set α) :
def right_coset_equivalence {α : Type u_1} [has_mul α] (s : set α) (a b : α) :
Prop

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

Equations
• = a = b)
def right_add_coset_equivalence {α : Type u_1} [has_add α] (s : set α) (a b : α) :
Prop

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

Equations
• = a = b)
theorem right_add_coset_equivalence_rel {α : Type u_1} [has_add α] (s : set α) :
theorem right_coset_equivalence_rel {α : Type u_1} [has_mul α] (s : set α) :
@[simp]
theorem left_add_coset_assoc {α : Type u_1} (s : set α) (a b : α) :
s) = left_add_coset (a + b) s
@[simp]
theorem left_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
s) = left_coset (a * b) s
@[simp]
theorem right_coset_assoc {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
right_coset a) b = (a * b)
@[simp]
theorem right_add_coset_assoc {α : Type u_1} (s : set α) (a b : α) :
b = (a + b)
theorem left_coset_right_coset {α : Type u_1} [semigroup α] (s : set α) (a b : α) :
right_coset s) b = b)
theorem left_add_coset_right_add_coset {α : Type u_1} (s : set α) (a b : α) :
b = b)
@[simp]
theorem zero_left_add_coset {α : Type u_1} [add_monoid α] (s : set α) :
= s
@[simp]
theorem one_left_coset {α : Type u_1} [monoid α] (s : set α) :
s = s
@[simp]
theorem right_add_coset_zero {α : Type u_1} [add_monoid α] (s : set α) :
= s
@[simp]
theorem right_coset_one {α : Type u_1} [monoid α] (s : set α) :
1 = s
theorem mem_own_left_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :
a s
a
theorem mem_own_right_coset {α : Type u_1} [monoid α] (s : submonoid α) (a : α) :
a a
a
a s
theorem mem_left_coset_left_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} (ha : s = s) :
a s
theorem mem_right_coset_right_coset {α : Type u_1} [monoid α] (s : submonoid α) {a : α} (ha : a = s) :
a s
a s
theorem mem_left_add_coset_iff {α : Type u_1} [add_group α] {s : set α} {x : α} (a : α) :
x -a + x s
theorem mem_left_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :
x s a⁻¹ * x s
theorem mem_right_coset_iff {α : Type u_1} [group α] {s : set α} {x : α} (a : α) :
x a x * a⁻¹ s
theorem mem_right_add_coset_iff {α : Type u_1} [add_group α] {s : set α} {x : α} (a : α) :
x x + -a s
theorem left_coset_mem_left_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : a s) :
s = s
= s
theorem right_coset_mem_right_coset {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : a s) :
a = s
= s
theorem orbit_subgroup_eq_right_coset {α : Type u_1} [group α] (s : subgroup α) (a : α) :
= a
theorem orbit_add_subgroup_eq_self_of_mem {α : Type u_1} [add_group α] (s : add_subgroup α) {a : α} (ha : a s) :
= s
theorem orbit_subgroup_eq_self_of_mem {α : Type u_1} [group α] (s : subgroup α) {a : α} (ha : a s) :
= s
= s
theorem orbit_subgroup_one_eq_self {α : Type u_1} [group α] (s : subgroup α) :
= s
theorem eq_cosets_of_normal {α : Type u_1} [group α] (s : subgroup α) (N : s.normal) (g : α) :
s = g
theorem eq_add_cosets_of_normal {α : Type u_1} [add_group α] (s : add_subgroup α) (N : s.normal) (g : α) :
=
theorem normal_of_eq_cosets {α : Type u_1} [group α] (s : subgroup α) (h : (g : α), s = g) :
theorem normal_of_eq_add_cosets {α : Type u_1} [add_group α] (s : add_subgroup α) (h : (g : α), = ) :
s.normal (g : α), =
theorem normal_iff_eq_cosets {α : Type u_1} [group α] (s : subgroup α) :
s.normal (g : α), s = g
theorem left_add_coset_eq_iff {α : Type u_1} [add_group α] (s : add_subgroup α) {x y : α} :
= -x + y s
theorem left_coset_eq_iff {α : Type u_1} [group α] (s : subgroup α) {x y : α} :
s = s x⁻¹ * y s
theorem right_coset_eq_iff {α : Type u_1} [group α] (s : subgroup α) {x y : α} :
x = y y * x⁻¹ s
theorem right_add_coset_eq_iff {α : Type u_1} [add_group α] (s : add_subgroup α) {x y : α} :
y + -x s

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

Equations
def quotient_group.left_rel {α : Type u_1} [group α] (s : subgroup α) :

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

Equations
theorem quotient_group.left_rel_apply {α : Type u_1} [group α] {s : subgroup α} {x y : α} :
y x⁻¹ * y s
theorem quotient_add_group.left_rel_apply {α : Type u_1} [add_group α] {s : add_subgroup α} {x y : α} :
y -x + y s
setoid.r = λ (x y : α), -x + y s
theorem quotient_group.left_rel_eq {α : Type u_1} [group α] (s : subgroup α) :
setoid.r = λ (x y : α), x⁻¹ * y s
@[protected, instance]
def quotient_group.left_rel_decidable {α : Type u_1} [group α] (s : subgroup α) [decidable_pred (λ (_x : α), _x s)] :
Equations
@[protected, instance]
def quotient_add_group.left_rel_decidable {α : Type u_1} [add_group α] (s : add_subgroup α) [decidable_pred (λ (_x : α), _x s)] :
Equations
• = λ (x y : α), _.mpr (_inst_2 (-x + y))
@[protected, instance]

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

Equations
@[protected, instance]

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

Equations
def quotient_group.right_rel {α : Type u_1} [group α] (s : subgroup α) :

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

Equations

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

Equations
theorem quotient_group.right_rel_apply {α : Type u_1} [group α] {s : subgroup α} {x y : α} :
y y * x⁻¹ s
theorem quotient_add_group.right_rel_apply {α : Type u_1} [add_group α] {s : add_subgroup α} {x y : α} :
y y + -x s
setoid.r = λ (x y : α), y + -x s
theorem quotient_group.right_rel_eq {α : Type u_1} [group α] (s : subgroup α) :
setoid.r = λ (x y : α), y * x⁻¹ s
@[protected, instance]
def quotient_group.right_rel_decidable {α : Type u_1} [group α] (s : subgroup α) [decidable_pred (λ (_x : α), _x s)] :
Equations
@[protected, instance]
def quotient_add_group.right_rel_decidable {α : Type u_1} [add_group α] (s : add_subgroup α) [decidable_pred (λ (_x : α), _x s)] :
Equations
• = λ (x y : α), _.mpr (_inst_2 (y + -x))

Right cosets are in bijection with left cosets.

Equations

Right cosets are in bijection with left cosets.

Equations
@[protected, instance]
def quotient_group.fintype_quotient_right_rel {α : Type u_1} [group α] (s : subgroup α) [fintype s)] :
Equations
@[protected, instance]
Equations
theorem quotient_group.card_quotient_right_rel {α : Type u_1} [group α] (s : subgroup α) [fintype s)] :
@[protected, instance]
def quotient_group.fintype {α : Type u_1} [group α] [fintype α] (s : subgroup α)  :
fintype s)
Equations
@[protected, instance]
fintype s)
Equations
@[reducible]
α s

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

@[reducible]
def quotient_group.mk {α : Type u_1} [group α] {s : subgroup α} (a : α) :
α s

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

theorem quotient_group.mk_surjective {α : Type u_1} [group α] {s : subgroup α} :
theorem quotient_group.induction_on {α : Type u_1} [group α] {s : subgroup α} {C : α s Prop} (x : α s) (H : (z : α), C ) :
C x
theorem quotient_add_group.induction_on {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α s Prop} (x : α s) (H : (z : α), ) :
C x
@[protected, instance]
Equations
@[protected, instance]
def quotient_group.has_quotient.quotient.has_coe_t {α : Type u_1} [group α] {s : subgroup α} :
s)
Equations
theorem quotient_add_group.induction_on' {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α s Prop} (x : α s) (H : (z : α), C z) :
C x
theorem quotient_group.induction_on' {α : Type u_1} [group α] {s : subgroup α} {C : α s Prop} (x : α s) (H : (z : α), C z) :
C x
@[simp]
theorem quotient_add_group.quotient_lift_on_coe {α : Type u_1} [add_group α] {s : add_subgroup α} {β : Sort u_2} (f : α β) (h : (a b : α), b f a = f b) (x : α) :
h = f x
@[simp]
theorem quotient_group.quotient_lift_on_coe {α : Type u_1} [group α] {s : subgroup α} {β : Sort u_2} (f : α β) (h : (a b : α), b f a = f b) (x : α) :
h = f x
theorem quotient_add_group.forall_coe {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α s Prop} :
( (x : α s), C x) (x : α), C x
theorem quotient_group.forall_coe {α : Type u_1} [group α] {s : subgroup α} {C : α s Prop} :
( (x : α s), C x) (x : α), C x
theorem quotient_add_group.exists_coe {α : Type u_1} [add_group α] {s : add_subgroup α} {C : α s Prop} :
( (x : α s), C x) (x : α), C x
theorem quotient_group.exists_coe {α : Type u_1} [group α] {s : subgroup α} {C : α s Prop} :
( (x : α s), C x) (x : α), C x
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem quotient_add_group.eq {α : Type u_1} [add_group α] {s : add_subgroup α} {a b : α} :
a = b -a + b s
@[protected]
theorem quotient_group.eq {α : Type u_1} [group α] {s : subgroup α} {a b : α} :
a = b a⁻¹ * b s
theorem quotient_add_group.eq' {α : Type u_1} [add_group α] {s : add_subgroup α} {a b : α} :
-a + b s
theorem quotient_group.eq' {α : Type u_1} [group α] {s : subgroup α} {a b : α} :
a⁻¹ * b s
@[simp]
theorem quotient_group.out_eq' {α : Type u_1} [group α] {s : subgroup α} (a : α s) :
@[simp]
theorem quotient_add_group.out_eq' {α : Type u_1} [add_group α] {s : add_subgroup α} (a : α s) :
(h : s),
theorem quotient_group.mk_out'_eq_mul {α : Type u_1} [group α] (s : subgroup α) (g : α) :
(h : s), = g * h
@[simp]
theorem quotient_add_group.mk_add_of_mem {α : Type u_1} [add_group α] {s : add_subgroup α} {b : α} (a : α) (hb : b s) :
@[simp]
theorem quotient_group.mk_mul_of_mem {α : Type u_1} [group α] {s : subgroup α} {b : α} (a : α) (hb : b s) :
theorem quotient_group.eq_class_eq_left_coset {α : Type u_1} [group α] (s : subgroup α) (g : α) :
{x : α | x = g} = s
{x : α | x = g} =
theorem quotient_group.preimage_image_coe {α : Type u_1} [group α] (N : subgroup α) (s : set α) :
coe ⁻¹' (coe '' s) = (x : N), (λ (y : α), y * x) ⁻¹' s
theorem quotient_add_group.preimage_image_coe {α : Type u_1} [add_group α] (N : add_subgroup α) (s : set α) :
coe ⁻¹' (coe '' s) = (x : N), (λ (y : α), y + x) ⁻¹' s
def subgroup.left_coset_equiv_subgroup {α : Type u_1} [group α] {s : subgroup α} (g : α) :

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

Equations

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

Equations
def subgroup.right_coset_equiv_subgroup {α : Type u_1} [group α] {s : subgroup α} (g : α) :
g) s

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

Equations
g) s

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

Equations
noncomputable def subgroup.group_equiv_quotient_times_subgroup {α : Type u_1} [group α] {s : subgroup α} :
α s) × s

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

Equations
α s) × s

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

Equations
def add_subgroup.quotient_equiv_of_eq {α : Type u_1} [add_group α] {s t : add_subgroup α} (h : s = t) :
α s α t

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

Equations
def subgroup.quotient_equiv_of_eq {α : Type u_1} [group α] {s t : subgroup α} (h : s = t) :
α s α t

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

Equations
theorem subgroup.quotient_equiv_of_eq_mk {α : Type u_1} [group α] {s t : subgroup α} (h : s = t) (a : α) :
@[simp]
theorem subgroup.quotient_equiv_prod_of_le'_symm_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s t) (f : α t α) (a : t) × t s.subgroup_of t) :
hf).symm) a = quotient.map' (λ (b : t), f a.fst * b) _ a.snd
def subgroup.quotient_equiv_prod_of_le' {α : Type u_1} [group α] {s t : subgroup α} (h_le : s t) (f : α t α)  :
α s t) × t s.subgroup_of t

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

Equations
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le'_symm_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s t) (f : α t α) (a : t) × t ) :
hf).symm) a = quotient.map' (λ (b : t), f a.fst + b) _ a.snd
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le'_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s t) (f : α t α) (a : α s) :
hf) a = a, quotient.map' (λ (g : α), -f (quotient.mk' g) + g, _⟩) _ a)
def add_subgroup.quotient_equiv_sum_of_le' {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s t) (f : α t α)  :
α s t) × t

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

Equations
@[simp]
theorem subgroup.quotient_equiv_prod_of_le'_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s t) (f : α t α) (a : α s) :
hf) a = a, quotient.map' (λ (g : α), (f (quotient.mk' g))⁻¹ * g, _⟩) _ a)
@[simp]
theorem subgroup.quotient_equiv_prod_of_le_symm_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s t) (a : t) × t s.subgroup_of t) :
.symm) a = quotient.map' (λ (b : t), * b) _ a.snd
noncomputable def add_subgroup.quotient_equiv_sum_of_le {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s t) :
α s t) × t

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

Equations
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s t) (a : α s) :
= a, quotient.map' (λ (g : α), -(quotient.mk' g).out' + g, _⟩) _ a)
@[simp]
theorem add_subgroup.quotient_equiv_sum_of_le_symm_apply {α : Type u_1} [add_group α] {s t : add_subgroup α} (h_le : s t) (a : t) × t ) :
a = quotient.map' (λ (b : t), + b) _ a.snd
noncomputable def subgroup.quotient_equiv_prod_of_le {α : Type u_1} [group α] {s t : subgroup α} (h_le : s t) :
α s t) × t s.subgroup_of t

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

Equations
• = subgroup.quotient_equiv_prod_of_le._proof_1
@[simp]
theorem subgroup.quotient_equiv_prod_of_le_apply {α : Type u_1} [group α] {s t : subgroup α} (h_le : s t) (a : α s) :
= a, quotient.map' (λ (g : α), ((quotient.mk' g).out')⁻¹ * g, _⟩) _ a)

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

Equations
def subgroup.quotient_subgroup_of_embedding_of_le {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s t) :

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

Equations
@[simp]
theorem subgroup.quotient_subgroup_of_embedding_of_le_apply_mk {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s t) (g : s) :
@[simp]

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

Equations
def subgroup.quotient_subgroup_of_map_of_le {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s t) :

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

Equations
@[simp]
@[simp]
theorem subgroup.quotient_subgroup_of_map_of_le_apply_mk {α : Type u_1} [group α] {s t : subgroup α} (H : subgroup α) (h : s t) (g : H) :
def subgroup.quotient_map_of_le {α : Type u_1} [group α] {s t : subgroup α} (h : s t) :
α s α t

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

Equations
def add_subgroup.quotient_map_of_le {α : Type u_1} [add_group α] {s t : add_subgroup α} (h : s t) :
α s α t

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

Equations
@[simp]
theorem subgroup.quotient_map_of_le_apply_mk {α : Type u_1} [group α] {s t : subgroup α} (h : s t) (g : α) :
@[simp]
theorem add_subgroup.quotient_map_of_le_apply_mk {α : Type u_1} [add_group α] {s t : add_subgroup α} (h : s t) (g : α) :
@[simp]
theorem subgroup.quotient_infi_subgroup_of_embedding_apply {α : Type u_1} [group α] {ι : Type u_2} (f : ι ) (H : subgroup α) (q : H ( (i : ι), f i).subgroup_of H) (i : ι) :
def subgroup.quotient_infi_subgroup_of_embedding {α : Type u_1} [group α] {ι : Type u_2} (f : ι ) (H : subgroup α) :
H ( (i : ι), f i).subgroup_of H Π (i : ι), H (f i).subgroup_of H

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

Equations
H ( (i : ι), f i).add_subgroup_of H Π (i : ι), H (f i).add_subgroup_of H

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

Equations
@[simp]
theorem add_subgroup.quotient_infi_add_subgroup_of_embedding_apply {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι ) (H : add_subgroup α) (q : H ( (i : ι), f i).add_subgroup_of H) (i : ι) :
@[simp]
theorem add_subgroup.quotient_infi_add_subgroup_of_embedding_apply_mk {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι ) (H : add_subgroup α) (g : H) (i : ι) :
@[simp]
theorem subgroup.quotient_infi_subgroup_of_embedding_apply_mk {α : Type u_1} [group α] {ι : Type u_2} (f : ι ) (H : subgroup α) (g : H) (i : ι) :
@[simp]
theorem add_subgroup.quotient_infi_embedding_apply {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι ) (q : α (i : ι), f i) (i : ι) :
@[simp]
theorem subgroup.quotient_infi_embedding_apply {α : Type u_1} [group α] {ι : Type u_2} (f : ι ) (q : α (i : ι), f i) (i : ι) :
def subgroup.quotient_infi_embedding {α : Type u_1} [group α] {ι : Type u_2} (f : ι ) :
(i : ι), f i) Π (i : ι), α f i

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

Equations
def add_subgroup.quotient_infi_embedding {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι ) :
(i : ι), f i) Π (i : ι), α f i

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

Equations
@[simp]
theorem subgroup.quotient_infi_embedding_apply_mk {α : Type u_1} [group α] {ι : Type u_2} (f : ι ) (g : α) (i : ι) :
@[simp]
theorem add_subgroup.quotient_infi_embedding_apply_mk {α : Type u_1} [add_group α] {ι : Type u_2} (f : ι ) (g : α) (i : ι) :
theorem subgroup.card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype s] [decidable_pred (λ (a : α), a s)] :
= fintype.card s) *

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

theorem subgroup.card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype s] :

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

theorem subgroup.card_quotient_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [decidable_pred (λ (_x : α), _x s)] :
theorem add_subgroup.card_quotient_dvd_card {α : Type u_1} [add_group α] [fintype α] (s : add_subgroup α) [decidable_pred (λ (_x : α), _x s)] :
theorem add_subgroup.card_dvd_of_injective {α : Type u_1} [add_group α] {H : Type u_2} [add_group H] [fintype α] [fintype H] (f : α →+ H) (hf : function.injective f) :
theorem subgroup.card_dvd_of_injective {α : Type u_1} [group α] {H : Type u_2} [group H] [fintype α] [fintype H] (f : α →* H) (hf : function.injective f) :
theorem subgroup.card_dvd_of_le {α : Type u_1} [group α] {H K : subgroup α} [fintype H] [fintype K] (hHK : H K) :
theorem add_subgroup.card_dvd_of_le {α : Type u_1} [add_group α] {H K : add_subgroup α} [fintype H] [fintype K] (hHK : H K) :
theorem subgroup.card_comap_dvd_of_injective {α : Type u_1} [group α] {H : Type u_2} [group H] (K : subgroup H) [fintype K] (f : α →* H) [fintype K)] (hf : function.injective f) :
theorem add_subgroup.card_comap_dvd_of_injective {α : Type u_1} [add_group α] {H : Type u_2} [add_group H] (K : add_subgroup H) [fintype K] (f : α →+ H) [fintype K)] (hf : function.injective f) :
noncomputable def quotient_group.preimage_mk_equiv_subgroup_times_set {α : Type u_1} [group α] (s : subgroup α) (t : set s)) :

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

Equations
If `s` is a subgroup of the additive group `α`, and `t` is a subset of `α ⧸ s`, then there is a (typically non-canonical) bijection between the preimage of `t` in `α` and the product `s × t`.
We use the class `has_coe_t` instead of `has_coe` if the first argument is a variable, or if the second argument is a variable not occurring in the first. Using `has_coe` would cause looping of type-class inference. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/remove.20all.20instances.20with.20variable.20domain