# mathlibdocumentation

deprecated.subgroup

# Unbundled subgroups (deprecated) #

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines unbundled multiplicative and additive subgroups. Instead of using this file, please use subgroup G and add_subgroup A, defined in group_theory.subgroup.basic.

## Main definitions #

is_add_subgroup (S : set A) : the predicate that S is the underlying subset of an additive subgroup of A. The bundled variant add_subgroup A should be used in preference to this.

is_subgroup (S : set G) : the predicate that S is the underlying subset of a subgroup of G. The bundled variant subgroup G should be used in preference to this.

## Tags #

subgroup, subgroups, is_subgroup

structure is_add_subgroup {A : Type u_3} [add_group A] (s : set A) :
Prop
• neg_mem : ∀ {a : A}, a s-a s

s is an additive subgroup: a set containing 0 and closed under addition and negation.

structure is_subgroup {G : Type u_1} [group G] (s : set G) :
Prop
• to_is_submonoid :
• inv_mem : ∀ {a : G}, a sa⁻¹ s

s is a subgroup: a set containing 1 and closed under multiplication and inverse.

theorem is_subgroup.div_mem {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) {x y : G} (hx : x s) (hy : y s) :
x / y s
theorem is_add_subgroup.sub_mem {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) {x y : G} (hx : x s) (hy : y s) :
x - y s
theorem additive.is_add_subgroup {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
theorem additive.is_add_subgroup_iff {G : Type u_1} [group G] {s : set G} :
theorem multiplicative.is_subgroup {A : Type u_3} [add_group A] {s : set A} (hs : is_add_subgroup s) :
theorem multiplicative.is_subgroup_iff {A : Type u_3} [add_group A] {s : set A} :
theorem is_subgroup.of_div {G : Type u_1} [group G] (s : set G) (one_mem : 1 s) (div_mem : ∀ {a b : G}, a sb sa * b⁻¹ s) :
theorem is_add_subgroup.of_add_neg {G : Type u_1} [add_group G] (s : set G) (one_mem : 0 s) (div_mem : ∀ {a b : G}, a sb sa + -b s) :
theorem is_add_subgroup.of_sub {A : Type u_3} [add_group A] (s : set A) (zero_mem : 0 s) (sub_mem : ∀ {a b : A}, a sb sa - b s) :
theorem is_subgroup.inter {G : Type u_1} [group G] {s₁ s₂ : set G} (hs₁ : is_subgroup s₁) (hs₂ : is_subgroup s₂) :
is_subgroup (s₁ s₂)
theorem is_subgroup.Inter {G : Type u_1} [group G] {ι : Sort u_2} {s : ι → set G} (hs : ∀ (y : ι), is_subgroup (s y)) :
theorem is_add_subgroup.Inter {G : Type u_1} [add_group G] {ι : Sort u_2} {s : ι → set G} (hs : ∀ (y : ι), is_add_subgroup (s y)) :
theorem is_add_subgroup_Union_of_directed {G : Type u_1} [add_group G] {ι : Type u_2} [hι : nonempty ι] {s : ι → set G} (hs : ∀ (i : ι), is_add_subgroup (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_add_subgroup (⋃ (i : ι), s i)
theorem is_subgroup_Union_of_directed {G : Type u_1} [group G] {ι : Type u_2} [hι : nonempty ι] {s : ι → set G} (hs : ∀ (i : ι), is_subgroup (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i s k s j s k) :
is_subgroup (⋃ (i : ι), s i)
theorem is_add_subgroup.neg_mem_iff {G : Type u_1} {a : G} [add_group G] {s : set G} (hs : is_add_subgroup s) :
-a s a s
theorem is_subgroup.inv_mem_iff {G : Type u_1} {a : G} [group G] {s : set G} (hs : is_subgroup s) :
a⁻¹ s a s
theorem is_subgroup.mul_mem_cancel_right {G : Type u_1} {a b : G} [group G] {s : set G} (hs : is_subgroup s) (h : a s) :
b * a s b s
theorem is_add_subgroup.add_mem_cancel_right {G : Type u_1} {a b : G} [add_group G] {s : set G} (hs : is_add_subgroup s) (h : a s) :
b + a s b s
theorem is_add_subgroup.add_mem_cancel_left {G : Type u_1} {a b : G} [add_group G] {s : set G} (hs : is_add_subgroup s) (h : a s) :
a + b s b s
theorem is_subgroup.mul_mem_cancel_left {G : Type u_1} {a b : G} [group G] {s : set G} (hs : is_subgroup s) (h : a s) :
a * b s b s
structure is_normal_add_subgroup {A : Type u_3} [add_group A] (s : set A) :
Prop
• normal : ∀ (n : A), n s∀ (g : A), g + n + -g s

is_normal_add_subgroup (s : set A) expresses the fact that s is a normal additive subgroup of the additive group A. Important: the preferred way to say this in Lean is via bundled subgroups S : add_subgroup A and hs : S.normal, and not via this structure.

structure is_normal_subgroup {G : Type u_1} [group G] (s : set G) :
Prop
• to_is_subgroup :
• normal : ∀ (n : G), n s∀ (g : G), g * n * g⁻¹ s

is_normal_subgroup (s : set G) expresses the fact that s is a normal subgroup of the group G. Important: the preferred way to say this in Lean is via bundled subgroups S : subgroup G and not via this structure.

theorem is_normal_subgroup_of_comm_group {G : Type u_1} [comm_group G] {s : set G} (hs : is_subgroup s) :
theorem additive.is_normal_add_subgroup {G : Type u_1} [group G] {s : set G} (hs : is_normal_subgroup s) :
theorem additive.is_normal_add_subgroup_iff {G : Type u_1} [group G] {s : set G} :
theorem multiplicative.is_normal_subgroup {A : Type u_3} [add_group A] {s : set A} (hs : is_normal_add_subgroup s) :
theorem multiplicative.is_normal_subgroup_iff {A : Type u_3} [add_group A] {s : set A} :
theorem is_subgroup.mem_norm_comm {G : Type u_1} [group G] {s : set G} (hs : is_normal_subgroup s) {a b : G} (hab : a * b s) :
b * a s
theorem is_add_subgroup.mem_norm_comm {G : Type u_1} [add_group G] {s : set G} (hs : is_normal_add_subgroup s) {a b : G} (hab : a + b s) :
b + a s
theorem is_add_subgroup.mem_norm_comm_iff {G : Type u_1} [add_group G] {s : set G} (hs : is_normal_add_subgroup s) {a b : G} :
a + b s b + a s
theorem is_subgroup.mem_norm_comm_iff {G : Type u_1} [group G] {s : set G} (hs : is_normal_subgroup s) {a b : G} :
a * b s b * a s
set G

Equations
def is_subgroup.trivial (G : Type u_1) [group G] :
set G

The trivial subgroup

Equations
• = {1}
@[simp]
theorem is_add_subgroup.mem_trivial {G : Type u_1} [add_group G] {g : G} :
g = 0
@[simp]
theorem is_subgroup.mem_trivial {G : Type u_1} [group G] {g : G} :
g = 1
theorem is_subgroup.trivial_normal {G : Type u_1} [group G] :
theorem is_add_subgroup.eq_trivial_iff {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) :
∀ (x : G), x sx = 0
theorem is_subgroup.eq_trivial_iff {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
∀ (x : G), x sx = 1
theorem is_subgroup.univ_subgroup {G : Type u_1} [group G] :
set G

The underlying set of the center of an additive group.

Equations
• = {z : G | ∀ (g : G), g + z = z + g}
def is_subgroup.center (G : Type u_1) [group G] :
set G

The underlying set of the center of a group.

Equations
• = {z : G | ∀ (g : G), g * z = z * g}
∀ (g : G), g + a = a + g
theorem is_subgroup.mem_center {G : Type u_1} [group G] {a : G} :
∀ (g : G), g * a = a * g
theorem is_subgroup.center_normal {G : Type u_1} [group G] :
set G

The underlying set of the normalizer of a subset S : set A of an additive group A. That is, the elements a : A such that a + S - a = S.

Equations
def is_subgroup.normalizer {G : Type u_1} [group G] (s : set G) :
set G

The underlying set of the normalizer of a subset S : set G of a group G. That is, the elements g : G such that g * S * g⁻¹ = S.

Equations
theorem is_subgroup.normalizer_is_subgroup {G : Type u_1} [group G] (s : set G) :
theorem is_subgroup.subset_normalizer {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
def is_group_hom.ker {G : Type u_1} {H : Type u_2} [group H] (f : G → H) :
set G

ker f : set G is the underlying subset of the kernel of a map G → H.

Equations
def is_add_group_hom.ker {G : Type u_1} {H : Type u_2} [add_group H] (f : G → H) :
set G

ker f : set A is the underlying subset of the kernel of a map A → B

Equations
theorem is_group_hom.mem_ker {G : Type u_1} {H : Type u_2} [group H] (f : G → H) {x : G} :
f x = 1
theorem is_add_group_hom.mem_ker {G : Type u_1} {H : Type u_2} [add_group H] (f : G → H) {x : G} :
f x = 0
theorem is_add_group_hom.zero_ker_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f (a + -b) = 0) :
f a = f b
theorem is_group_hom.one_ker_inv {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f (a * b⁻¹) = 1) :
f a = f b
theorem is_add_group_hom.zero_ker_neg' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f (-a + b) = 0) :
f a = f b
theorem is_group_hom.one_ker_inv' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f (a⁻¹ * b) = 1) :
f a = f b
theorem is_add_group_hom.neg_ker_zero {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f a = f b) :
f (a + -b) = 0
theorem is_group_hom.inv_ker_one {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f a = f b) :
f (a * b⁻¹) = 1
theorem is_add_group_hom.neg_ker_zero' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {a b : G} (h : f a = f b) :
f (-a + b) = 0
theorem is_group_hom.inv_ker_one' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {a b : G} (h : f a = f b) :
f (a⁻¹ * b) = 1
theorem is_add_group_hom.zero_iff_ker_neg {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
f a = f b f (a + -b) = 0
theorem is_group_hom.one_iff_ker_inv {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
f a = f b f (a * b⁻¹) = 1
theorem is_group_hom.one_iff_ker_inv' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
f a = f b f (a⁻¹ * b) = 1
theorem is_add_group_hom.zero_iff_ker_neg' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
f a = f b f (-a + b) = 0
theorem is_add_group_hom.neg_iff_ker {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
f a = f b a + -b
theorem is_group_hom.inv_iff_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
f a = f b a * b⁻¹
theorem is_add_group_hom.neg_iff_ker' {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (a b : G) :
f a = f b -a + b
theorem is_group_hom.inv_iff_ker' {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (a b : G) :
f a = f b a⁻¹ * b
theorem is_group_hom.image_subgroup {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {s : set G} (hs : is_subgroup s) :
theorem is_group_hom.range_subgroup {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
theorem is_group_hom.preimage {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {s : set H} (hs : is_subgroup s) :
theorem is_add_group_hom.preimage {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {s : set H} (hs : is_add_subgroup s) :
theorem is_add_group_hom.preimage_normal {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) {s : set H} (hs : is_normal_add_subgroup s) :
theorem is_group_hom.preimage_normal {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) {s : set H} (hs : is_normal_subgroup s) :
theorem is_group_hom.is_normal_subgroup_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
theorem is_add_group_hom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f)  :
theorem is_group_hom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (h : = ) :
theorem is_add_group_hom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (h : function.injective f) :
theorem is_group_hom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (h : function.injective f) :
theorem is_add_group_hom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) :
theorem is_group_hom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
theorem is_add_group_hom.trivial_ker_iff_eq_zero {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) :
∀ (x : G), f x = 0x = 0
theorem is_group_hom.trivial_ker_iff_eq_one {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) :
∀ (x : G), f x = 1x = 1
inductive add_group.in_closure {A : Type u_3} [add_group A] (s : set A) :
A → Prop
• basic : ∀ {A : Type u_3} [_inst_1 : {s : set A} {a : A}, a s
• zero : ∀ {A : Type u_3} [_inst_1 : {s : set A},
• neg : ∀ {A : Type u_3} [_inst_1 : {s : set A} {a : A},
• add : ∀ {A : Type u_3} [_inst_1 : {s : set A} {a b : A}, (a + b)

If A is an additive group and s : set A, then in_closure s : set A is the underlying subset of the subgroup generated by s.

inductive group.in_closure {G : Type u_1} [group G] (s : set G) :
G → Prop
• basic : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G} {a : G}, a s
• one : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G},
• inv : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G} {a : G},
• mul : ∀ {G : Type u_1} [_inst_1 : group G] {s : set G} {a b : G}, (a * b)

If G is a group and s : set G, then in_closure s : set G is the underlying subset of the subgroup generated by s.

def add_group.closure {G : Type u_1} [add_group G] (s : set G) :
set G

add_group.closure s is the additive subgroup generated by s, i.e., the smallest additive subgroup containing s.

Equations
• = {a : G |
def group.closure {G : Type u_1} [group G] (s : set G) :
set G

group.closure s is the subgroup generated by s, i.e. the smallest subgroup containg s.

Equations
• = {a : G | a}
theorem add_group.mem_closure {G : Type u_1} [add_group G] {s : set G} {a : G} :
a s
theorem group.mem_closure {G : Type u_1} [group G] {s : set G} {a : G} :
a s
theorem group.closure.is_subgroup {G : Type u_1} [group G] (s : set G) :
theorem group.subset_closure {G : Type u_1} [group G] {s : set G} :
theorem add_group.subset_closure {G : Type u_1} [add_group G] {s : set G} :
theorem add_group.closure_subset {G : Type u_1} [add_group G] {s t : set G} (ht : is_add_subgroup t) (h : s t) :
theorem group.closure_subset {G : Type u_1} [group G] {s t : set G} (ht : is_subgroup t) (h : s t) :
theorem add_group.closure_subset_iff {G : Type u_1} [add_group G] {s t : set G} (ht : is_add_subgroup t) :
s t
theorem group.closure_subset_iff {G : Type u_1} [group G] {s t : set G} (ht : is_subgroup t) :
s t
theorem add_group.closure_mono {G : Type u_1} [add_group G] {s t : set G} (h : s t) :
theorem group.closure_mono {G : Type u_1} [group G] {s t : set G} (h : s t) :
@[simp]
@[simp]
theorem group.closure_subgroup {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
theorem group.exists_list_of_mem_closure {G : Type u_1} [group G] {s : set G} {a : G} (h : a ) :
∃ (l : list G), (∀ (x : G), x lx s x⁻¹ s) l.prod = a
theorem add_group.exists_list_of_mem_closure {G : Type u_1} [add_group G] {s : set G} {a : G} (h : a ) :
∃ (l : list G), (∀ (x : G), x lx s -x s) l.sum = a
theorem add_group.image_closure {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {f : G → H} (hf : is_add_group_hom f) (s : set G) :
theorem group.image_closure {G : Type u_1} {H : Type u_2} [group G] [group H] {f : G → H} (hf : is_group_hom f) (s : set G) :
theorem group.mclosure_subset {G : Type u_1} [group G] {s : set G} :
theorem add_group.mclosure_subset {G : Type u_1} [add_group G] {s : set G} :
theorem add_group.mclosure_neg_subset {G : Type u_1} [add_group G] {s : set G} :
theorem group.mclosure_inv_subset {G : Type u_1} [group G] {s : set G} :
theorem add_group.closure_eq_mclosure {G : Type u_1} [add_group G] {s : set G} :
theorem group.closure_eq_mclosure {G : Type u_1} [group G] {s : set G} :
theorem add_group.mem_closure_union_iff {G : Type u_1} {s t : set G} {x : G} :
x add_group.closure (s t) ∃ (y : G) (H : (z : G) (H : , y + z = x
theorem group.mem_closure_union_iff {G : Type u_1} [comm_group G] {s t : set G} {x : G} :
x group.closure (s t) ∃ (y : G) (H : y (z : G) (H : z , y * z = x
theorem is_subgroup.trivial_eq_closure {G : Type u_1} [group G] :
theorem group.conjugates_of_subset {G : Type u_1} [group G] {t : set G} (ht : is_normal_subgroup t) {a : G} (h : a t) :
theorem group.conjugates_of_set_subset' {G : Type u_1} [group G] {s t : set G} (ht : is_normal_subgroup t) (h : s t) :
def group.normal_closure {G : Type u_1} [group G] (s : set G) :
set G

The normal closure of a set s is the subgroup closure of all the conjugates of elements of s. It is the smallest normal subgroup containing s.

Equations
theorem group.conjugates_of_set_subset_normal_closure {G : Type u_1} {s : set G} [group G] :
theorem group.subset_normal_closure {G : Type u_1} {s : set G} [group G] :
theorem group.normal_closure.is_subgroup {G : Type u_1} [group G] (s : set G) :

The normal closure of a set is a subgroup.

theorem group.normal_closure.is_normal {G : Type u_1} {s : set G} [group G] :

The normal closure of s is a normal subgroup.

theorem group.normal_closure_subset {G : Type u_1} [group G] {s t : set G} (ht : is_normal_subgroup t) (h : s t) :

The normal closure of s is the smallest normal subgroup containing s.

theorem group.normal_closure_subset_iff {G : Type u_1} [group G] {s t : set G} (ht : is_normal_subgroup t) :
s t
theorem group.normal_closure_mono {G : Type u_1} [group G] {s t : set G} :
s t
def subgroup.of {G : Type u_1} [group G] {s : set G} (h : is_subgroup s) :

Create a bundled subgroup from a set s and [is_subgroup s].

Equations
def add_subgroup.of {G : Type u_1} [add_group G] {s : set G} (h : is_add_subgroup s) :

Create a bundled additive subgroup from a set s and [is_add_subgroup s].

Equations