mathlib3 documentation

deprecated.subgroup

Unbundled subgroups (deprecated) #

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

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

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

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 multiplicative.is_subgroup {A : Type u_3} [add_group A] {s : set A} (hs : is_add_subgroup s) :
theorem is_subgroup.of_div {G : Type u_1} [group G] (s : set G) (one_mem : 1 s) (div_mem : {a b : G}, a s b s a * 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 s b s a + -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 s b s a - b s) :
theorem is_add_subgroup.inter {G : Type u_1} [add_group G] {s₁ s₂ : set G} (hs₁ : is_add_subgroup s₁) (hs₂ : is_add_subgroup s₂) :
is_add_subgroup (s₁ 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

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

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_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
def is_add_subgroup.trivial (G : Type u_1) [add_group G] :
set G

the trivial additive subgroup

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

The trivial subgroup

Equations
@[simp]
theorem is_add_subgroup.mem_trivial {G : Type u_1} [add_group G] {g : G} :
@[simp]
theorem is_subgroup.mem_trivial {G : Type u_1} [group G] {g : G} :
theorem is_add_subgroup.eq_trivial_iff {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) :
s = is_add_subgroup.trivial G (x : G), x s x = 0
theorem is_subgroup.eq_trivial_iff {G : Type u_1} [group G] {s : set G} (hs : is_subgroup s) :
s = is_subgroup.trivial G (x : G), x s x = 1
def is_add_subgroup.add_center (G : Type u_1) [add_group G] :
set G

The underlying set of the center of an additive group.

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

The underlying set of the center of a group.

Equations
theorem is_add_subgroup.mem_add_center {G : Type u_1} [add_group G] {a : G} :
a is_add_subgroup.add_center G (g : G), g + a = a + g
theorem is_subgroup.mem_center {G : Type u_1} [group G] {a : G} :
a is_subgroup.center G (g : G), g * a = a * g
def is_add_subgroup.add_normalizer {G : Type u_1} [add_group G] (s : set 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
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} :
theorem is_add_group_hom.mem_ker {G : Type u_1} {H : Type u_2} [add_group H] (f : G H) {x : G} :
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) :
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) :
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) :
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) :
theorem is_add_group_hom.image_add_subgroup {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} (hs : is_add_subgroup s) :
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.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) :
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) :
inductive add_group.in_closure {A : Type u_3} [add_group A] (s : set A) :
A Prop

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

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
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
theorem add_group.mem_closure {G : Type u_1} [add_group G] {s : set G} {a : G} :
theorem group.mem_closure {G : Type u_1} [group G] {s : set G} {a : G} :
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) :
theorem group.closure_subset_iff {G : Type u_1} [group G] {s t : set G} (ht : is_subgroup 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]
theorem add_group.closure_add_subgroup {G : Type u_1} [add_group G] {s : set G} (hs : is_add_subgroup s) :
@[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 group.closure s) :
(l : list G), ( (x : G), x l x 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 add_group.closure s) :
(l : list G), ( (x : G), x l x 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.mem_closure_union_iff {G : Type u_1} [add_comm_group G] {s t : set G} {x : G} :
x add_group.closure (s t) (y : G) (H : y add_group.closure s) (z : G) (H : z add_group.closure t), 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 group.closure s) (z : G) (H : z group.closure t), y * z = x
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

The normal closure of a set is a subgroup.

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.

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
theorem subgroup.is_subgroup {G : Type u_1} [group G] (K : subgroup G) :
theorem subgroup.of_normal {G : Type u_1} [group G] (s : set G) (h : is_subgroup s) (n : is_normal_subgroup s) :