# Documentation

Mathlib.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 AddSubgroup A, defined in GroupTheory.Subgroup.Basic.

## Main definitions #

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

IsSubgroup (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, IsSubgroup

structure IsAddSubgroup {A : Type u_1} [inst : ] (s : Set A) extends :
• The proposition that s is closed under negation.

neg_mem : ∀ {a : A}, a s-a s

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

Instances For
structure IsSubgroup {G : Type u_1} [inst : ] (s : Set G) extends :
• The proposition that s is closed under inverse.

inv_mem : ∀ {a : G}, a sa⁻¹ s

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

Instances For
theorem IsAddSubgroup.sub_mem {G : Type u_1} [inst : ] {s : Set G} (hs : ) {x : G} {y : G} (hx : x s) (hy : y s) :
x - y s
theorem IsSubgroup.div_mem {G : Type u_1} [inst : ] {s : Set G} (hs : ) {x : G} {y : G} (hx : x s) (hy : y s) :
x / y s
theorem Additive.isAddSubgroup {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
theorem Additive.isAddSubgroup_iff {G : Type u_1} [inst : ] {s : Set G} :
theorem Multiplicative.isSubgroup {A : Type u_1} [inst : ] {s : Set A} (hs : ) :
theorem Multiplicative.isSubgroup_iff {A : Type u_1} [inst : ] {s : Set A} :
theorem IsAddSubgroup.of_add_neg {G : Type u_1} [inst : ] (s : Set G) (one_mem : 0 s) (div_mem : ∀ {a b : G}, a sb sa + -b s) :
theorem IsSubgroup.of_div {G : Type u_1} [inst : ] (s : Set G) (one_mem : 1 s) (div_mem : ∀ {a b : G}, a sb sa * b⁻¹ s) :
theorem IsAddSubgroup.of_sub {A : Type u_1} [inst : ] (s : Set A) (zero_mem : 0 s) (sub_mem : ∀ {a b : A}, a sb sa - b s) :
theorem IsAddSubgroup.inter {G : Type u_1} [inst : ] {s₁ : Set G} {s₂ : Set G} (hs₁ : ) (hs₂ : ) :
theorem IsSubgroup.inter {G : Type u_1} [inst : ] {s₁ : Set G} {s₂ : Set G} (hs₁ : ) (hs₂ : ) :
IsSubgroup (s₁ s₂)
theorem IsAddSubgroup.interᵢ {G : Type u_2} [inst : ] {ι : Sort u_1} {s : ιSet G} (hs : ∀ (y : ι), IsAddSubgroup (s y)) :
theorem IsSubgroup.interᵢ {G : Type u_2} [inst : ] {ι : Sort u_1} {s : ιSet G} (hs : ∀ (y : ι), IsSubgroup (s y)) :
abbrev isAddSubgroup_unionᵢ_of_directed.match_1 {G : Type u_2} {ι : Type u_1} {s : ιSet G} :
{a : G} → (motive : (i, a s i) → Prop) → ∀ (x : i, a s i), (∀ (i : ι) (hi : a s i), motive (_ : i, a s i)) → motive x
Equations
theorem isAddSubgroup_unionᵢ_of_directed {G : Type u_2} [inst : ] {ι : Type u_1} [inst : ] {s : ιSet G} (hs : ∀ (i : ι), IsAddSubgroup (s i)) (directed : ∀ (i j : ι), k, s i s k s j s k) :
theorem isSubgroup_unionᵢ_of_directed {G : Type u_2} [inst : ] {ι : Type u_1} [inst : ] {s : ιSet G} (hs : ∀ (i : ι), IsSubgroup (s i)) (directed : ∀ (i j : ι), k, s i s k s j s k) :
IsSubgroup (Set.unionᵢ fun i => s i)
theorem IsAddSubgroup.neg_mem_iff {G : Type u_1} {a : G} [inst : ] {s : Set G} (hs : ) :
-a s a s
theorem IsSubgroup.inv_mem_iff {G : Type u_1} {a : G} [inst : ] {s : Set G} (hs : ) :
a⁻¹ s a s
theorem IsAddSubgroup.add_mem_cancel_right {G : Type u_1} {a : G} {b : G} [inst : ] {s : Set G} (hs : ) (h : a s) :
b + a s b s
theorem IsSubgroup.mul_mem_cancel_right {G : Type u_1} {a : G} {b : G} [inst : ] {s : Set G} (hs : ) (h : a s) :
b * a s b s
theorem IsAddSubgroup.add_mem_cancel_left {G : Type u_1} {a : G} {b : G} [inst : ] {s : Set G} (hs : ) (h : a s) :
a + b s b s
theorem IsSubgroup.mul_mem_cancel_left {G : Type u_1} {a : G} {b : G} [inst : ] {s : Set G} (hs : ) (h : a s) :
a * b s b s
structure IsNormalAddSubgroup {A : Type u_1} [inst : ] (s : Set A) extends :
• The proposition that s is closed under (additive) conjugation.

normal : ∀ (n : A), n s∀ (g : A), g + n + -g s

IsNormalAddSubgroup (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 : AddSubgroup A and hs : S.normal, and not via this structure.

Instances For
structure IsNormalSubgroup {G : Type u_1} [inst : ] (s : Set G) extends :
• The proposition that s is closed under conjugation.

normal : ∀ (n : G), n s∀ (g : G), g * n * g⁻¹ s

IsNormalSubgroup (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.

Instances For
theorem isNormalAddSubgroup_of_addCommGroup {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
theorem isNormalSubgroup_of_commGroup {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
theorem Additive.isNormalAddSubgroup {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
theorem Additive.isNormalAddSubgroup_iff {G : Type u_1} [inst : ] {s : Set G} :
theorem Multiplicative.isNormalSubgroup {A : Type u_1} [inst : ] {s : Set A} (hs : ) :
theorem Multiplicative.isNormalSubgroup_iff {A : Type u_1} [inst : ] {s : Set A} :
theorem IsAddSubgroup.mem_norm_comm {G : Type u_1} [inst : ] {s : Set G} (hs : ) {a : G} {b : G} (hab : a + b s) :
b + a s
theorem IsSubgroup.mem_norm_comm {G : Type u_1} [inst : ] {s : Set G} (hs : ) {a : G} {b : G} (hab : a * b s) :
b * a s
theorem IsAddSubgroup.mem_norm_comm_iff {G : Type u_1} [inst : ] {s : Set G} (hs : ) {a : G} {b : G} :
a + b s b + a s
theorem IsSubgroup.mem_norm_comm_iff {G : Type u_1} [inst : ] {s : Set G} (hs : ) {a : G} {b : G} :
a * b s b * a s
def IsAddSubgroup.trivial (G : Type u_1) [inst : ] :
Set G

Equations
def IsSubgroup.trivial (G : Type u_1) [inst : ] :
Set G

The trivial subgroup

Equations
• = {1}
@[simp]
theorem IsAddSubgroup.mem_trivial {G : Type u_1} [inst : ] {g : G} :
g = 0
@[simp]
theorem IsSubgroup.mem_trivial {G : Type u_1} [inst : ] {g : G} :
g = 1
theorem IsAddSubgroup.trivial_normal {G : Type u_1} [inst : ] :
theorem IsSubgroup.trivial_normal {G : Type u_1} [inst : ] :
theorem IsAddSubgroup.eq_trivial_iff {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
∀ (x : G), x sx = 0
theorem IsSubgroup.eq_trivial_iff {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
∀ (x : G), x sx = 1
theorem IsSubgroup.univ_subgroup {G : Type u_1} [inst : ] :
Set G

The underlying set of the center of an additive group.

Equations
• = { z | ∀ (g : G), g + z = z + g }
def IsSubgroup.center (G : Type u_1) [inst : ] :
Set G

The underlying set of the center of a group.

Equations
• = { z | ∀ (g : G), g * z = z * g }
theorem IsAddSubgroup.mem_add_center {G : Type u_1} [inst : ] {a : G} :
∀ (g : G), g + a = a + g
theorem IsSubgroup.mem_center {G : Type u_1} [inst : ] {a : G} :
∀ (g : G), g * a = a * g
theorem IsSubgroup.center_normal {G : Type u_1} [inst : ] :
def IsAddSubgroup.addNormalizer {G : Type u_1} [inst : ] (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 IsSubgroup.normalizer {G : Type u_1} [inst : ] (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 IsAddSubgroup.normalizer_isAddSubgroup {G : Type u_1} [inst : ] (s : Set G) :
theorem IsSubgroup.normalizer_isSubgroup {G : Type u_1} [inst : ] (s : Set G) :
theorem IsAddSubgroup.subset_add_normalizer {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
theorem IsSubgroup.subset_normalizer {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
def IsAddGroupHom.ker {G : Type u_1} {H : Type u_2} [inst : ] (f : GH) :
Set G

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

Equations
def IsGroupHom.ker {G : Type u_1} {H : Type u_2} [inst : ] (f : GH) :
Set G

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

Equations
theorem IsAddGroupHom.mem_ker {G : Type u_2} {H : Type u_1} [inst : ] (f : GH) {x : G} :
f x = 0
theorem IsGroupHom.mem_ker {G : Type u_2} {H : Type u_1} [inst : ] (f : GH) {x : G} :
f x = 1
theorem IsAddGroupHom.zero_ker_neg {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f (a + -b) = 0) :
f a = f b
theorem IsGroupHom.one_ker_inv {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f (a * b⁻¹) = 1) :
f a = f b
theorem IsAddGroupHom.zero_ker_neg' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f (-a + b) = 0) :
f a = f b
theorem IsGroupHom.one_ker_inv' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f (a⁻¹ * b) = 1) :
f a = f b
theorem IsAddGroupHom.neg_ker_zero {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f a = f b) :
f (a + -b) = 0
theorem IsGroupHom.inv_ker_one {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f a = f b) :
f (a * b⁻¹) = 1
theorem IsAddGroupHom.neg_ker_zero' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f a = f b) :
f (-a + b) = 0
theorem IsGroupHom.inv_ker_one' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {a : G} {b : G} (h : f a = f b) :
f (a⁻¹ * b) = 1
theorem IsAddGroupHom.zero_iff_ker_neg {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b f (a + -b) = 0
theorem IsGroupHom.one_iff_ker_inv {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b f (a * b⁻¹) = 1
theorem IsAddGroupHom.zero_iff_ker_neg' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b f (-a + b) = 0
theorem IsGroupHom.one_iff_ker_inv' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b f (a⁻¹ * b) = 1
theorem IsAddGroupHom.neg_iff_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b a + -b
theorem IsGroupHom.inv_iff_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b a * b⁻¹
theorem IsAddGroupHom.neg_iff_ker' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b -a + b
theorem IsGroupHom.inv_iff_ker' {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (a : G) (b : G) :
f a = f b a⁻¹ * b
abbrev IsAddGroupHom.image_addSubgroup.match_1 {G : Type u_2} {H : Type u_1} {f : GH} {s : Set G} {a₂ : H} (motive : a₂ f '' sProp) :
(x : a₂ f '' s) → ((b₂ : G) → (hb₂ : b₂ s) → (eq₂ : f b₂ = a₂) → motive (_ : a, a s f a = a₂)) → motive x
Equations
theorem IsAddGroupHom.image_addSubgroup {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {s : Set G} (hs : ) :
theorem IsGroupHom.image_subgroup {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {s : Set G} (hs : ) :
theorem IsAddGroupHom.range_addSubgroup {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
theorem IsGroupHom.range_subgroup {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
theorem IsAddGroupHom.preimage {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {s : Set H} (hs : ) :
theorem IsGroupHom.preimage {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {s : Set H} (hs : ) :
theorem IsAddGroupHom.preimage_normal {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {s : Set H} (hs : ) :
theorem IsGroupHom.preimage_normal {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) {s : Set H} (hs : ) :
theorem IsAddGroupHom.isNormalAddSubgroup_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
theorem IsGroupHom.isNormalSubgroup_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
theorem IsAddGroupHom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (h : ) :
theorem IsGroupHom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (h : ) :
theorem IsAddGroupHom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (h : ) :
theorem IsGroupHom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) (h : ) :
theorem IsAddGroupHom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
theorem IsGroupHom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
theorem IsAddGroupHom.trivial_ker_iff_eq_zero {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
∀ (x : G), f x = 0x = 0
theorem IsGroupHom.trivial_ker_iff_eq_one {G : Type u_1} {H : Type u_2} [inst : ] [inst : ] {f : GH} (hf : ) :
∀ (x : G), f x = 1x = 1
inductive AddGroup.InClosure {A : Type u_1} [inst : ] (s : Set A) :
AProp
• basic: ∀ {A : Type u_1} [inst : ] {s : Set A} {a : A}, a s
• zero: ∀ {A : Type u_1} [inst : ] {s : Set A},
• neg: ∀ {A : Type u_1} [inst : ] {s : Set A} {a : A},
• add: ∀ {A : Type u_1} [inst : ] {s : Set A} {a b : A}, AddGroup.InClosure s (a + b)

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

Instances For
inductive Group.InClosure {G : Type u_1} [inst : ] (s : Set G) :
GProp
• basic: ∀ {G : Type u_1} [inst : ] {s : Set G} {a : G}, a s
• one: ∀ {G : Type u_1} [inst : ] {s : Set G},
• inv: ∀ {G : Type u_1} [inst : ] {s : Set G} {a : G},
• mul: ∀ {G : Type u_1} [inst : ] {s : Set G} {a b : G}, Group.InClosure s (a * b)

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

Instances For
def AddGroup.closure {G : Type u_1} [inst : ] (s : Set G) :
Set G

Equations
• = { a | }
def Group.closure {G : Type u_1} [inst : ] (s : Set G) :
Set G

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

Equations
• = { a | }
theorem AddGroup.mem_closure {G : Type u_1} [inst : ] {s : Set G} {a : G} :
a s
theorem Group.mem_closure {G : Type u_1} [inst : ] {s : Set G} {a : G} :
a s
theorem AddGroup.closure.isAddSubgroup {G : Type u_1} [inst : ] (s : Set G) :
theorem Group.closure.isSubgroup {G : Type u_1} [inst : ] (s : Set G) :
theorem AddGroup.subset_closure {G : Type u_1} [inst : ] {s : Set G} :
theorem Group.subset_closure {G : Type u_1} [inst : ] {s : Set G} :
theorem AddGroup.closure_subset {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) (h : s t) :
theorem Group.closure_subset {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) (h : s t) :
theorem AddGroup.closure_subset_iff {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) :
s t
theorem Group.closure_subset_iff {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) :
s t
theorem AddGroup.closure_mono {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (h : s t) :
theorem Group.closure_mono {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (h : s t) :
@[simp]
theorem AddGroup.closure_addSubgroup {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
@[simp]
theorem Group.closure_subgroup {G : Type u_1} [inst : ] {s : Set G} (hs : ) :
theorem AddGroup.exists_list_of_mem_closure {G : Type u_1} [inst : ] {s : Set G} {a : G} (h : ) :
l, (∀ (x : G), x lx s -x s) = a
abbrev AddGroup.exists_list_of_mem_closure.match_1 {G : Type u_1} [inst : ] (L : List G) (x : G) (motive : (a, -a = x) → Prop) :
(x : a, -a = x) → ((y : G) → (hy1 : ) → (hy2 : -y = x) → motive (_ : a, -a = x)) → motive x
Equations
abbrev AddGroup.exists_list_of_mem_closure.match_2 {G : Type u_1} [inst : ] {s : Set G} {x : G} (motive : (l, (∀ (x : G), x lx s -x s) = x) → Prop) :
(x : l, (∀ (x : G), x lx s -x s) = x) → ((L : List G) → (HL1 : ∀ (x : G), x Lx s -x s) → (HL2 : = x) → motive (_ : l, (∀ (x : G), x lx s -x s) = x)) → motive x
Equations
theorem Group.exists_list_of_mem_closure {G : Type u_1} [inst : ] {s : Set G} {a : G} (h : ) :
l, (∀ (x : G), x lx s x⁻¹ s) = a
theorem AddGroup.image_closure {G : Type u_2} {H : Type u_1} [inst : ] [inst : ] {f : GH} (hf : ) (s : Set G) :
theorem Group.image_closure {G : Type u_2} {H : Type u_1} [inst : ] [inst : ] {f : GH} (hf : ) (s : Set G) :
theorem AddGroup.mclosure_subset {G : Type u_1} [inst : ] {s : Set G} :
theorem Group.mclosure_subset {G : Type u_1} [inst : ] {s : Set G} :
theorem AddGroup.mclosure_neg_subset {G : Type u_1} [inst : ] {s : Set G} :
theorem Group.mclosure_inv_subset {G : Type u_1} [inst : ] {s : Set G} :
theorem AddGroup.closure_eq_mclosure {G : Type u_1} [inst : ] {s : Set G} :
= AddMonoid.Closure (s Neg.neg ⁻¹' s)
theorem Group.closure_eq_mclosure {G : Type u_1} [inst : ] {s : Set G} :
= Monoid.Closure (s Inv.inv ⁻¹' s)
theorem AddGroup.mem_closure_union_iff {G : Type u_1} [inst : ] {s : Set G} {t : Set G} {x : G} :
x AddGroup.closure (s t) y, z, y + z = x
theorem Group.mem_closure_union_iff {G : Type u_1} [inst : ] {s : Set G} {t : Set G} {x : G} :
x Group.closure (s t) y, z, y * z = x
theorem IsAddSubgroup.trivial_eq_closure {G : Type u_1} [inst : ] :
theorem IsSubgroup.trivial_eq_closure {G : Type u_1} [inst : ] :
theorem Group.conjugatesOf_subset {G : Type u_1} [inst : ] {t : Set G} (ht : ) {a : G} (h : a t) :
theorem Group.conjugatesOfSet_subset' {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) (h : s t) :
def Group.normalClosure {G : Type u_1} [inst : ] (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.conjugatesOfSet_subset_normalClosure {G : Type u_1} {s : Set G} [inst : ] :
theorem Group.subset_normalClosure {G : Type u_1} {s : Set G} [inst : ] :
theorem Group.normalClosure.isSubgroup {G : Type u_1} [inst : ] (s : Set G) :

The normal closure of a set is a subgroup.

theorem Group.normalClosure.is_normal {G : Type u_1} {s : Set G} [inst : ] :

The normal closure of s is a normal subgroup.

theorem Group.normalClosure_subset {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) (h : s t) :

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

theorem Group.normalClosure_subset_iff {G : Type u_1} [inst : ] {s : Set G} {t : Set G} (ht : ) :
s t
theorem Group.normalClosure_mono {G : Type u_1} [inst : ] {s : Set G} {t : Set G} :
s t
def AddSubgroup.of.proof_1 {G : Type u_1} [inst : ] {s : Set G} (h : ) :
∀ {a b : G}, a sb sa + b s
Equations
def AddSubgroup.of.proof_3 {G : Type u_1} [inst : ] {s : Set G} (h : ) :
∀ {x : G}, x s-x s
Equations
def AddSubgroup.of {G : Type u_1} [inst : ] {s : Set G} (h : ) :

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

Equations
• One or more equations did not get rendered due to their size.
def AddSubgroup.of.proof_2 {G : Type u_1} [inst : ] {s : Set G} (h : ) :
0 s
Equations
def Subgroup.of {G : Type u_1} [inst : ] {s : Set G} (h : ) :

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

Equations
• One or more equations did not get rendered due to their size.
theorem AddSubgroup.isAddSubgroup {G : Type u_1} [inst : ] (K : ) :
theorem Subgroup.isSubgroup {G : Type u_1} [inst : ] (K : ) :
theorem AddSubgroup.of_normal {G : Type u_1} [inst : ] (s : Set G) (h : ) (n : ) :
theorem Subgroup.of_normal {G : Type u_1} [inst : ] (s : Set G) (h : ) (n : ) :