mathlib documentation

deprecated.subgroup

theorem additive.is_add_subgroup {G : Type u_1} [group G] (s : set G) [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) [is_add_subgroup s] :

def subtype.add_group {G : Type u_1} [add_group G] {s : set G} [is_add_subgroup s] :

The additive group structure on an additive subgroup coerced to a type.

def subtype.group {G : Type u_1} [group G] {s : set G} [is_subgroup s] :

The group structure on a subgroup coerced to a type.

Equations
def subtype.comm_group {G : Type u_1} [comm_group G] {s : set G} [is_subgroup s] :

The commutative group structure on a commutative subgroup coerced to a type.

Equations

The additive commutative group structure on a additive commutative subgroup coerced to a type.

@[simp]
theorem is_add_subgroup.coe_neg {G : Type u_1} [add_group G] {s : set G} [is_add_subgroup s] (a : s) :

@[simp]
theorem is_subgroup.coe_inv {G : Type u_1} [group G] {s : set G} [is_subgroup s] (a : s) :

@[simp]
theorem is_subgroup.coe_gpow {G : Type u_1} [group G] {s : set G} [is_subgroup s] (a : s) (n : ) :
(a ^ n) = a ^ n

@[simp]
theorem is_add_subgroup.gsmul_coe {A : Type u_3} [add_group A] {s : set A} [is_add_subgroup s] (a : s) (n : ) :

theorem is_subgroup.of_div {G : Type u_1} [group G] (s : set G) :
1 s(∀ {a b : G}, a sb sa * b⁻¹ s)is_subgroup s

theorem is_add_subgroup.of_add_neg {G : Type u_1} [add_group G] (s : set G) :
0 s(∀ {a b : G}, a sb sa + -b s)is_add_subgroup s

theorem is_add_subgroup.of_sub {A : Type u_3} [add_group A] (s : set A) :
0 s(∀ {a b : A}, a sb sa - b s)is_add_subgroup s

@[instance]
def is_add_subgroup.inter {G : Type u_1} [add_group G] (s₁ s₂ : set G) [is_add_subgroup s₁] [is_add_subgroup s₂] :
is_add_subgroup (s₁ s₂)

@[instance]
def is_subgroup.inter {G : Type u_1} [group G] (s₁ s₂ : set G) [is_subgroup s₁] [is_subgroup s₂] :
is_subgroup (s₁ s₂)

@[instance]
def is_subgroup.Inter {G : Type u_1} [group G] {ι : Sort u_2} (s : ι → set G) [h : ∀ (y : ι), is_subgroup (s y)] :

@[instance]
def is_add_subgroup.Inter {G : Type u_1} [add_group G] {ι : Sort u_2} (s : ι → set G) [h : ∀ (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) [∀ (i : ι), is_add_subgroup (s i)] :
(∀ (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) [∀ (i : ι), is_subgroup (s i)] :
(∀ (i j : ι), ∃ (k : ι), s i s k s j s k)is_subgroup (⋃ (i : ι), s i)

def gpowers {G : Type u_1} [group G] :
G → set G

Equations
def gmultiples {A : Type u_3} [add_group A] :
A → set A

Equations
@[instance]
def gpowers.is_subgroup {G : Type u_1} [group G] (x : G) :

@[instance]
def gmultiples.is_add_subgroup {A : Type u_3} [add_group A] (x : A) :

theorem is_subgroup.gpow_mem {G : Type u_1} [group G] {a : G} {s : set G} [is_subgroup s] (h : a s) {i : } :
a ^ i s

theorem is_add_subgroup.gsmul_mem {A : Type u_3} [add_group A] {a : A} {s : set A} [is_add_subgroup s] (a_1 : a s) {i : } :
i •ℤ a s

theorem gpowers_subset {G : Type u_1} [group G] {a : G} {s : set G} [is_subgroup s] :
a sgpowers a s

theorem gmultiples_subset {A : Type u_3} [add_group A] {a : A} {s : set A} [is_add_subgroup s] :
a sgmultiples a s

theorem mem_gpowers {G : Type u_1} [group G] {a : G} :

theorem mem_gmultiples {A : Type u_3} [add_group A] {a : A} :

theorem is_add_subgroup.neg_mem_iff {G : Type u_1} {a : G} [add_group G] (s : set G) [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) [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) [is_subgroup s] :
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) [is_add_subgroup s] :
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) [is_add_subgroup s] :
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) [is_subgroup s] :
a s(a * b s b s)

theorem is_add_subgroup.sub_mem {A : Type u_1} [add_group A] (s : set A) [is_add_subgroup s] (a b : A) :
a sb sa - b s

theorem normal_subgroup_of_comm_group {G : Type u_1} [comm_group G] (s : set G) [hs : is_subgroup s] :

theorem additive.normal_add_subgroup {G : Type u_1} [group G] (s : set G) [normal_subgroup s] :

theorem is_subgroup.mem_norm_comm {G : Type u_1} [group G] {s : set G} [normal_subgroup s] {a b : G} :
a * b sb * a s

theorem is_add_subgroup.mem_norm_comm {G : Type u_1} [add_group G] {s : set G} [normal_add_subgroup s] {a b : G} :
a + b sb + a s

theorem is_add_subgroup.mem_norm_comm_iff {G : Type u_1} [add_group G] {s : set G} [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} [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

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} :

@[instance]

theorem is_add_subgroup.eq_trivial_iff {G : Type u_1} [add_group G] {s : set G} [is_add_subgroup s] :
s = is_add_subgroup.trivial G ∀ (x : G), x sx = 0

theorem is_subgroup.eq_trivial_iff {G : Type u_1} [group G] {s : set G} [is_subgroup s] :
s = is_subgroup.trivial G ∀ (x : G), x sx = 1

@[instance]

def is_add_subgroup.add_center (G : Type u_1) [add_group G] :
set G

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

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

@[instance]

def is_add_subgroup.add_normalizer {G : Type u_1} [add_group G] :
set Gset G

def is_subgroup.normalizer {G : Type u_1} [group G] :
set Gset G

Equations
@[instance]

theorem is_subgroup.subset_normalizer {G : Type u_1} [group G] (s : set G) [is_subgroup s] :

@[instance]

Every subgroup is a normal subgroup of its normalizer

def is_group_hom.ker {G : Type u_1} {H : Type u_2} [group H] :
(G → H)set G

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

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) [is_add_group_hom f] {a b : G} :
f (a + -b) = 0f 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) [is_group_hom f] {a b : G} :
f (a * b⁻¹) = 1f 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) [is_add_group_hom f] {a b : G} :
f (-a + b) = 0f 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) [is_group_hom f] {a b : G} :
f (a⁻¹ * b) = 1f 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) [is_add_group_hom f] {a b : G} :
f a = f bf (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) [is_group_hom f] {a b : G} :
f a = f bf (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) [is_add_group_hom f] {a b : G} :
f a = f bf (-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) [is_group_hom f] {a b : G} :
f a = f bf (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) [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) [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) [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) [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) [w : 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) [w : 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) [w : 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) [w : is_group_hom f] (a b : G) :

@[instance]
def is_add_group_hom.image_add_subgroup {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G → H) [is_add_group_hom f] (s : set G) [is_add_subgroup s] :

@[instance]
def is_group_hom.image_subgroup {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G → H) [is_group_hom f] (s : set G) [is_subgroup s] :

@[instance]
def is_add_group_hom.range_add_subgroup {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G → H) [is_add_group_hom f] :

@[instance]
def is_group_hom.range_subgroup {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G → H) [is_group_hom f] :

@[instance]
def is_group_hom.preimage {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G → H) [is_group_hom f] (s : set H) [is_subgroup s] :

@[instance]
def is_add_group_hom.preimage {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G → H) [is_add_group_hom f] (s : set H) [is_add_subgroup s] :

@[instance]
def is_add_group_hom.preimage_normal {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G → H) [is_add_group_hom f] (s : set H) [normal_add_subgroup s] :

@[instance]
def is_group_hom.preimage_normal {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G → H) [is_group_hom f] (s : set H) [normal_subgroup s] :

@[instance]

@[instance]
def is_group_hom.normal_subgroup_ker {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G → H) [is_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) [is_group_hom f] :

theorem is_group_hom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G → H) [is_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) [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) [is_add_group_hom f] :
is_add_group_hom.ker f = is_add_subgroup.trivial G ∀ (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) [is_group_hom f] :
is_group_hom.ker f = is_subgroup.trivial G ∀ (x : G), f x = 1x = 1

@[instance]
def subtype_val.is_group_hom {G : Type u_1} [group G] {s : set G} [is_subgroup s] :

@[instance]
def coe.is_group_hom {G : Type u_1} [group G] {s : set G} [is_subgroup s] :

@[instance]
def coe.is_add_group_hom {G : Type u_1} [add_group G] {s : set G} [is_add_subgroup s] :

@[instance]
def subtype_mk.is_group_hom {G : Type u_1} {H : Type u_2} [group G] [group H] {s : set G} [is_subgroup s] (f : H → G) [is_group_hom f] (h : ∀ (x : H), f x s) :
is_group_hom (λ (x : H), f x, _⟩)

@[instance]
def subtype_mk.is_add_group_hom {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] {s : set G} [is_add_subgroup s] (f : H → G) [is_add_group_hom f] (h : ∀ (x : H), f x s) :
is_add_group_hom (λ (x : H), f x, _⟩)

@[instance]

@[instance]
def set_inclusion.is_group_hom {G : Type u_1} [group G] {s t : set G} [is_subgroup s] [is_subgroup t] (h : s t) :

def monoid_hom.range_subtype_val {G : Type u_1} {H : Type u_2} [monoid G] [monoid H] (f : G →* H) :

subtype.val : set.range f → H as a monoid homomorphism, when f is a monoid homomorphism.

Equations
def add_monoid_hom.range_subtype_val {G : Type u_1} {H : Type u_2} [add_monoid G] [add_monoid H] (f : G →+ H) :

subtype.val : set.range f → H as an additive monoid homomorphism, when f is an additive monoid homomorphism.

def add_monoid_hom.range_factorization {G : Type u_1} {H : Type u_2} [add_monoid G] [add_monoid H] (f : G →+ H) :

set.range_factorization f : G → set.range f as an additive monoid homomorphism, when f is an additive monoid homomorphism.

def monoid_hom.range_factorization {G : Type u_1} {H : Type u_2} [monoid G] [monoid H] (f : G →* H) :

set.range_factorization f : G → set.range f as a monoid homomorphism, when f is a monoid homomorphism.

Equations
inductive add_group.in_closure {A : Type u_3} [add_group A] :
set AA → Prop

inductive group.in_closure {G : Type u_1} [group G] :
set GG → Prop

def add_group.closure {G : Type u_1} [add_group G] :
set Gset G

def group.closure {G : Type u_1} [group G] :
set Gset G

group.closure s is the subgroup closed over 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} :
a sa group.closure s

@[instance]
def group.closure.is_subgroup {G : Type u_1} [group G] (s : set G) :

@[instance]

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} [is_add_subgroup t] :

theorem group.closure_subset {G : Type u_1} [group G] {s t : set G} [is_subgroup t] :
s tgroup.closure s t

theorem add_group.closure_subset_iff {G : Type u_1} [add_group G] (s t : set G) [is_add_subgroup t] :

theorem group.closure_subset_iff {G : Type u_1} [group G] (s t : set G) [is_subgroup t] :

theorem add_group.closure_mono {G : Type u_1} [add_group G] {s t : set G} :

theorem group.closure_mono {G : Type u_1} [group G] {s t : set G} :

@[simp]
theorem add_group.closure_add_subgroup {G : Type u_1} [add_group G] (s : set G) [is_add_subgroup s] :

@[simp]
theorem group.closure_subgroup {G : Type u_1} [group G] (s : set G) [is_subgroup s] :

theorem group.exists_list_of_mem_closure {G : Type u_1} [group G] {s : set G} {a : G} :
a group.closure s(∃ (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} :
a add_group.closure s(∃ (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) [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) [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 add_group.gmultiples_eq_closure {G : Type u_1} [add_group G] {a : G} :

theorem group.gpowers_eq_closure {G : Type u_1} [group G] {a : G} :

theorem group.conjugates_subset {G : Type u_1} [group G] {t : set G} [normal_subgroup t] {a : G} :

theorem group.conjugates_of_set_subset' {G : Type u_1} [group G] {s t : set G} [normal_subgroup t] :

def group.normal_closure {G : Type u_1} [group G] :
set Gset 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.subset_normal_closure {G : Type u_1} {s : set G} [group G] :

@[instance]

The normal closure of a set is a subgroup.

@[instance]

The normal closure of s is a normal subgroup.

theorem group.normal_closure_subset {G : Type u_1} [group G] {s t : set G} [normal_subgroup 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} [normal_subgroup t] :

theorem group.normal_closure_mono {G : Type u_1} [group G] {s t : set G} :

@[class]
structure simple_group (G : Type u_4) [group G] :
Prop

Instances
@[class]
structure simple_add_group (A : Type u_4) [add_group A] :
Prop

Instances
@[instance]

theorem simple_group_of_surjective {G : Type u_1} {H : Type u_2} [group G] [group H] [simple_group G] (f : G → H) [is_group_hom f] :

theorem simple_add_group_of_surjective {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] [simple_add_group G] (f : G → H) [is_add_group_hom f] :

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_subroup 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].

@[instance]

@[instance]
def subgroup.is_subgroup {G : Type u_1} [group G] (K : subgroup G) :

@[instance]
def subgroup.of_normal {G : Type u_1} [group G] (s : set G) [h : is_subgroup s] [n : normal_subgroup s] :

@[instance]
def add_subgroup.of_normal {G : Type u_1} [add_group G] (s : set G) [h : is_add_subgroup s] [n : normal_add_subgroup s] :