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 Mathlib.Algebra.Group.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_3} [AddGroup A] (s : Set A) extends IsAddSubmonoid :

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

zero_mem : 0 ∈ s
add_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s
neg_mem : ∀ {a : A}, a ∈ s → -a ∈ s
The proposition that s is closed under negation.

Instances For

theorem IsAddSubgroup.neg_mem {A : Type u_3} [AddGroup A] {s : Set A} (self : IsAddSubgroup s) {a : A} :

a ∈ s → -a ∈ s

The proposition that s is closed under negation.

structure IsSubgroup {G : Type u_1} [Group G] (s : Set G) extends IsSubmonoid :

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

one_mem : 1 ∈ s
mul_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s
inv_mem : ∀ {a : G}, a ∈ s → a⁻¹ ∈ s
The proposition that s is closed under inverse.

Instances For

theorem IsSubgroup.inv_mem {G : Type u_1} [Group G] {s : Set G} (self : IsSubgroup s) {a : G} :

a ∈ s → a⁻¹ ∈ s

The proposition that s is closed under inverse.

theorem IsAddSubgroup.sub_mem {G : Type u_1} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) {x : G} {y : G} (hx : x ∈ s) (hy : y ∈ s) :

x - y ∈ s

theorem IsSubgroup.div_mem {G : Type u_1} [Group G] {s : Set G} (hs : IsSubgroup s) {x : G} {y : G} (hx : x ∈ s) (hy : y ∈ s) :

x / y ∈ s

theorem Additive.isAddSubgroup {G : Type u_1} [Group G] {s : Set G} (hs : IsSubgroup s) :

IsAddSubgroup s

theorem Additive.isAddSubgroup_iff {G : Type u_1} [Group G] {s : Set G} :

IsAddSubgroup s ↔ IsSubgroup s

theorem Multiplicative.isSubgroup {A : Type u_3} [AddGroup A] {s : Set A} (hs : IsAddSubgroup s) :

theorem Multiplicative.isSubgroup_iff {A : Type u_3} [AddGroup A] {s : Set A} :

IsSubgroup s ↔ IsAddSubgroup s

theorem IsAddSubgroup.of_add_neg {G : Type u_1} [AddGroup G] (s : Set G) (one_mem : 0 ∈ s) (div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a + -b ∈ s) :

IsAddSubgroup s

theorem IsSubgroup.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 IsAddSubgroup.of_sub {A : Type u_3} [AddGroup A] (s : Set A) (zero_mem : 0 ∈ s) (sub_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a - b ∈ s) :

IsAddSubgroup s

theorem IsAddSubgroup.inter {G : Type u_1} [AddGroup G] {s₁ : Set G} {s₂ : Set G} (hs₁ : IsAddSubgroup s₁) (hs₂ : IsAddSubgroup s₂) :

IsAddSubgroup (s₁ ∩ s₂)

theorem IsSubgroup.inter {G : Type u_1} [Group G] {s₁ : Set G} {s₂ : Set G} (hs₁ : IsSubgroup s₁) (hs₂ : IsSubgroup s₂) :

IsSubgroup (s₁ ∩ s₂)

theorem IsAddSubgroup.iInter {G : Type u_1} [AddGroup G] {ι : Sort u_4} {s : ι → Set G} (hs : ∀ (y : ι), IsAddSubgroup (s y)) :

IsAddSubgroup (Set.iInter s)

theorem IsSubgroup.iInter {G : Type u_1} [Group G] {ι : Sort u_4} {s : ι → Set G} (hs : ∀ (y : ι), IsSubgroup (s y)) :

IsSubgroup (Set.iInter s)

theorem isAddSubgroup_iUnion_of_directed {G : Type u_1} [AddGroup G] {ι : Type u_4} [Nonempty ι] {s : ι → Set G} (hs : ∀ (i : ι), IsAddSubgroup (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) :

IsAddSubgroup (⋃ (i : ι), s i)

theorem isSubgroup_iUnion_of_directed {G : Type u_1} [Group G] {ι : Type u_4} [Nonempty ι] {s : ι → Set G} (hs : ∀ (i : ι), IsSubgroup (s i)) (directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) :

IsSubgroup (⋃ (i : ι), s i)

theorem IsAddSubgroup.neg_mem_iff {G : Type u_1} {a : G} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) :

-a ∈ s ↔ a ∈ s

theorem IsSubgroup.inv_mem_iff {G : Type u_1} {a : G} [Group G] {s : Set G} (hs : IsSubgroup s) :

a⁻¹ ∈ s ↔ a ∈ s

theorem IsAddSubgroup.add_mem_cancel_right {G : Type u_1} {a : G} {b : G} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) (h : a ∈ s) :

b + a ∈ s ↔ b ∈ s

theorem IsSubgroup.mul_mem_cancel_right {G : Type u_1} {a : G} {b : G} [Group G] {s : Set G} (hs : IsSubgroup s) (h : a ∈ s) :

b * a ∈ s ↔ b ∈ s

theorem IsAddSubgroup.add_mem_cancel_left {G : Type u_1} {a : G} {b : G} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) (h : a ∈ s) :

a + b ∈ s ↔ b ∈ s

theorem IsSubgroup.mul_mem_cancel_left {G : Type u_1} {a : G} {b : G} [Group G] {s : Set G} (hs : IsSubgroup s) (h : a ∈ s) :

a * b ∈ s ↔ b ∈ s

structure IsNormalAddSubgroup {A : Type u_3} [AddGroup A] (s : Set A) extends IsAddSubgroup :

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.

zero_mem : 0 ∈ s
add_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s
neg_mem : ∀ {a : A}, a ∈ s → -a ∈ s
normal : ∀ n ∈ s, ∀ (g : A), g + n + -g ∈ s
The proposition that s is closed under (additive) conjugation.

Instances For

theorem IsNormalAddSubgroup.normal {A : Type u_3} [AddGroup A] {s : Set A} (self : IsNormalAddSubgroup s) (n : A) :

n ∈ s → ∀ (g : A), g + n + -g ∈ s

The proposition that s is closed under (additive) conjugation.

structure IsNormalSubgroup {G : Type u_1} [Group G] (s : Set G) extends IsSubgroup :

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.

one_mem : 1 ∈ s
mul_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s
inv_mem : ∀ {a : G}, a ∈ s → a⁻¹ ∈ s
normal : ∀ n ∈ s, ∀ (g : G), g * n * g⁻¹ ∈ s
The proposition that s is closed under conjugation.

Instances For

theorem IsNormalSubgroup.normal {G : Type u_1} [Group G] {s : Set G} (self : IsNormalSubgroup s) (n : G) :

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

The proposition that s is closed under conjugation.

theorem isNormalAddSubgroup_of_addCommGroup {G : Type u_1} [AddCommGroup G] {s : Set G} (hs : IsAddSubgroup s) :

IsNormalAddSubgroup s

theorem isNormalSubgroup_of_commGroup {G : Type u_1} [CommGroup G] {s : Set G} (hs : IsSubgroup s) :

IsNormalSubgroup s

theorem Additive.isNormalAddSubgroup {G : Type u_1} [Group G] {s : Set G} (hs : IsNormalSubgroup s) :

IsNormalAddSubgroup s

theorem Additive.isNormalAddSubgroup_iff {G : Type u_1} [Group G] {s : Set G} :

IsNormalAddSubgroup s ↔ IsNormalSubgroup s

theorem Multiplicative.isNormalSubgroup {A : Type u_3} [AddGroup A] {s : Set A} (hs : IsNormalAddSubgroup s) :

IsNormalSubgroup s

theorem Multiplicative.isNormalSubgroup_iff {A : Type u_3} [AddGroup A] {s : Set A} :

IsNormalSubgroup s ↔ IsNormalAddSubgroup s

theorem IsAddSubgroup.mem_norm_comm {G : Type u_1} [AddGroup G] {s : Set G} (hs : IsNormalAddSubgroup s) {a : G} {b : G} (hab : a + b ∈ s) :

b + a ∈ s

theorem IsSubgroup.mem_norm_comm {G : Type u_1} [Group G] {s : Set G} (hs : IsNormalSubgroup s) {a : G} {b : G} (hab : a * b ∈ s) :

b * a ∈ s

theorem IsAddSubgroup.mem_norm_comm_iff {G : Type u_1} [AddGroup G] {s : Set G} (hs : IsNormalAddSubgroup s) {a : G} {b : G} :

a + b ∈ s ↔ b + a ∈ s

theorem IsSubgroup.mem_norm_comm_iff {G : Type u_1} [Group G] {s : Set G} (hs : IsNormalSubgroup s) {a : G} {b : G} :

a * b ∈ s ↔ b * a ∈ s

def IsAddSubgroup.trivial (G : Type u_4) [AddGroup G] :

the trivial additive subgroup

Equations

IsAddSubgroup.trivial G = {0}

Instances For

def IsSubgroup.trivial (G : Type u_4) [Group G] :

The trivial subgroup

Equations

IsSubgroup.trivial G = {1}

Instances For

@[simp]

theorem IsAddSubgroup.mem_trivial {G : Type u_1} [AddGroup G] {g : G} :

g ∈ IsAddSubgroup.trivial G ↔ g = 0

@[simp]

theorem IsSubgroup.mem_trivial {G : Type u_1} [Group G] {g : G} :

g ∈ IsSubgroup.trivial G ↔ g = 1

theorem IsAddSubgroup.trivial_normal {G : Type u_1} [AddGroup G] :

IsNormalAddSubgroup (IsAddSubgroup.trivial G)

theorem IsSubgroup.trivial_normal {G : Type u_1} [Group G] :

IsNormalSubgroup (IsSubgroup.trivial G)

theorem IsAddSubgroup.eq_trivial_iff {G : Type u_1} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) :

s = IsAddSubgroup.trivial G ↔ ∀ x ∈ s, x = 0

theorem IsSubgroup.eq_trivial_iff {G : Type u_1} [Group G] {s : Set G} (hs : IsSubgroup s) :

s = IsSubgroup.trivial G ↔ ∀ x ∈ s, x = 1

theorem IsAddSubgroup.univ_addSubgroup {G : Type u_1} [AddGroup G] :

IsNormalAddSubgroup Set.univ

theorem IsSubgroup.univ_subgroup {G : Type u_1} [Group G] :

IsNormalSubgroup Set.univ

def IsAddSubgroup.addCenter (G : Type u_4) [AddGroup G] :

The underlying set of the center of an additive group.

Equations

IsAddSubgroup.addCenter G = {z : G | ∀ (g : G), g + z = z + g}

Instances For

def IsSubgroup.center (G : Type u_4) [Group G] :

The underlying set of the center of a group.

Equations

IsSubgroup.center G = {z : G | ∀ (g : G), g * z = z * g}

Instances For

theorem IsAddSubgroup.mem_add_center {G : Type u_1} [AddGroup G] {a : G} :

a ∈ IsAddSubgroup.addCenter G ↔ ∀ (g : G), g + a = a + g

theorem IsSubgroup.mem_center {G : Type u_1} [Group G] {a : G} :

a ∈ IsSubgroup.center G ↔ ∀ (g : G), g * a = a * g

theorem IsAddSubgroup.add_center_normal {G : Type u_1} [AddGroup G] :

IsNormalAddSubgroup (IsAddSubgroup.addCenter G)

theorem IsSubgroup.center_normal {G : Type u_1} [Group G] :

IsNormalSubgroup (IsSubgroup.center G)

def IsAddSubgroup.addNormalizer {G : Type u_1} [AddGroup G] (s : 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

IsAddSubgroup.addNormalizer s = {g : G | ∀ (n : G), n ∈ s ↔ g + n + -g ∈ s}

Instances For

def IsSubgroup.normalizer {G : Type u_1} [Group G] (s : 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

IsSubgroup.normalizer s = {g : G | ∀ (n : G), n ∈ s ↔ g * n * g⁻¹ ∈ s}

Instances For

theorem IsAddSubgroup.normalizer_isAddSubgroup {G : Type u_1} [AddGroup G] (s : Set G) :

IsAddSubgroup (IsAddSubgroup.addNormalizer s)

theorem IsSubgroup.normalizer_isSubgroup {G : Type u_1} [Group G] (s : Set G) :

IsSubgroup (IsSubgroup.normalizer s)

theorem IsAddSubgroup.subset_add_normalizer {G : Type u_1} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) :

s ⊆ IsAddSubgroup.addNormalizer s

theorem IsSubgroup.subset_normalizer {G : Type u_1} [Group G] {s : Set G} (hs : IsSubgroup s) :

s ⊆ IsSubgroup.normalizer s

def IsAddGroupHom.ker {G : Type u_1} {H : Type u_2} [AddGroup H] (f : G → H) :

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

Equations

IsAddGroupHom.ker f = f ⁻¹' IsAddSubgroup.trivial H

Instances For

def IsGroupHom.ker {G : Type u_1} {H : Type u_2} [Group H] (f : G → H) :

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

Equations

IsGroupHom.ker f = f ⁻¹' IsSubgroup.trivial H

Instances For

theorem IsAddGroupHom.mem_ker {G : Type u_1} {H : Type u_2} [AddGroup H] (f : G → H) {x : G} :

x ∈ IsAddGroupHom.ker f ↔ f x = 0

theorem IsGroupHom.mem_ker {G : Type u_1} {H : Type u_2} [Group H] (f : G → H) {x : G} :

x ∈ IsGroupHom.ker f ↔ f x = 1

theorem IsAddGroupHom.zero_ker_neg {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {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} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {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} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {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} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {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} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {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} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {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} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {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} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {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} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (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} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (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} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (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} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (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} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (a : G) (b : G) :

f a = f b ↔ a + -b ∈ IsAddGroupHom.ker f

theorem IsGroupHom.inv_iff_ker {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (a : G) (b : G) :

f a = f b ↔ a * b⁻¹ ∈ IsGroupHom.ker f

theorem IsAddGroupHom.neg_iff_ker' {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (a : G) (b : G) :

f a = f b ↔ -a + b ∈ IsAddGroupHom.ker f

theorem IsGroupHom.inv_iff_ker' {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (a : G) (b : G) :

f a = f b ↔ a⁻¹ * b ∈ IsGroupHom.ker f

theorem IsAddGroupHom.image_addSubgroup {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {s : Set G} (hs : IsAddSubgroup s) :

IsAddSubgroup (f '' s)

theorem IsGroupHom.image_subgroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {s : Set G} (hs : IsSubgroup s) :

IsSubgroup (f '' s)

theorem IsAddGroupHom.range_addSubgroup {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) :

IsAddSubgroup (Set.range f)

theorem IsGroupHom.range_subgroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) :

IsSubgroup (Set.range f)

theorem IsAddGroupHom.preimage {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {s : Set H} (hs : IsAddSubgroup s) :

IsAddSubgroup (f ⁻¹' s)

theorem IsGroupHom.preimage {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {s : Set H} (hs : IsSubgroup s) :

IsSubgroup (f ⁻¹' s)

theorem IsAddGroupHom.preimage_normal {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) {s : Set H} (hs : IsNormalAddSubgroup s) :

IsNormalAddSubgroup (f ⁻¹' s)

theorem IsGroupHom.preimage_normal {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) {s : Set H} (hs : IsNormalSubgroup s) :

IsNormalSubgroup (f ⁻¹' s)

theorem IsAddGroupHom.isNormalAddSubgroup_ker {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) :

IsNormalAddSubgroup (IsAddGroupHom.ker f)

theorem IsGroupHom.isNormalSubgroup_ker {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) :

IsNormalSubgroup (IsGroupHom.ker f)

theorem IsAddGroupHom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (h : IsAddGroupHom.ker f = IsAddSubgroup.trivial G) :

Function.Injective f

theorem IsGroupHom.injective_of_trivial_ker {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (h : IsGroupHom.ker f = IsSubgroup.trivial G) :

Function.Injective f

theorem IsAddGroupHom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (h : Function.Injective f) :

IsAddGroupHom.ker f = IsAddSubgroup.trivial G

theorem IsGroupHom.trivial_ker_of_injective {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (h : Function.Injective f) :

IsGroupHom.ker f = IsSubgroup.trivial G

theorem IsAddGroupHom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) :

Function.Injective f ↔ IsAddGroupHom.ker f = IsAddSubgroup.trivial G

theorem IsGroupHom.injective_iff_trivial_ker {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) :

Function.Injective f ↔ IsGroupHom.ker f = IsSubgroup.trivial G

theorem IsAddGroupHom.trivial_ker_iff_eq_zero {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) :

IsAddGroupHom.ker f = IsAddSubgroup.trivial G ↔ ∀ (x : G), f x = 0 → x = 0

theorem IsGroupHom.trivial_ker_iff_eq_one {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) :

IsGroupHom.ker f = IsSubgroup.trivial G ↔ ∀ (x : G), f x = 1 → x = 1

inductive AddGroup.InClosure {A : Type u_3} [AddGroup A] (s : Set A) :

A → Prop

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.

basic: ∀ {A : Type u_3} [inst : AddGroup A] {s : Set A} {a : A}, a ∈ s → AddGroup.InClosure s a
zero: ∀ {A : Type u_3} [inst : AddGroup A] {s : Set A}, AddGroup.InClosure s 0
neg: ∀ {A : Type u_3} [inst : AddGroup A] {s : Set A} {a : A}, AddGroup.InClosure s a → AddGroup.InClosure s (-a)
add: ∀ {A : Type u_3} [inst : AddGroup A] {s : Set A} {a b : A}, AddGroup.InClosure s a → AddGroup.InClosure s b → AddGroup.InClosure s (a + b)

Instances For

inductive Group.InClosure {G : Type u_1} [Group G] (s : Set G) :

G → Prop

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

basic: ∀ {G : Type u_1} [inst : Group G] {s : Set G} {a : G}, a ∈ s → Group.InClosure s a
one: ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Group.InClosure s 1
inv: ∀ {G : Type u_1} [inst : Group G] {s : Set G} {a : G}, Group.InClosure s a → Group.InClosure s a⁻¹
mul: ∀ {G : Type u_1} [inst : Group G] {s : Set G} {a b : G}, Group.InClosure s a → Group.InClosure s b → Group.InClosure s (a * b)

Instances For

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

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

Equations

AddGroup.closure s = {a : G | AddGroup.InClosure s a}

Instances For

def Group.closure {G : Type u_1} [Group G] (s : Set G) :

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

Equations

Group.closure s = {a : G | Group.InClosure s a}

Instances For

theorem AddGroup.mem_closure {G : Type u_1} [AddGroup G] {s : Set G} {a : G} :

a ∈ s → a ∈ AddGroup.closure s

theorem Group.mem_closure {G : Type u_1} [Group G] {s : Set G} {a : G} :

a ∈ s → a ∈ Group.closure s

theorem AddGroup.closure.isAddSubgroup {G : Type u_1} [AddGroup G] (s : Set G) :

IsAddSubgroup (AddGroup.closure s)

theorem Group.closure.isSubgroup {G : Type u_1} [Group G] (s : Set G) :

IsSubgroup (Group.closure s)

theorem AddGroup.subset_closure {G : Type u_1} [AddGroup G] {s : Set G} :

s ⊆ AddGroup.closure s

theorem Group.subset_closure {G : Type u_1} [Group G] {s : Set G} :

s ⊆ Group.closure s

theorem AddGroup.closure_subset {G : Type u_1} [AddGroup G] {s : Set G} {t : Set G} (ht : IsAddSubgroup t) (h : s ⊆ t) :

AddGroup.closure s ⊆ t

theorem Group.closure_subset {G : Type u_1} [Group G] {s : Set G} {t : Set G} (ht : IsSubgroup t) (h : s ⊆ t) :

Group.closure s ⊆ t

theorem AddGroup.closure_subset_iff {G : Type u_1} [AddGroup G] {s : Set G} {t : Set G} (ht : IsAddSubgroup t) :

AddGroup.closure s ⊆ t ↔ s ⊆ t

theorem Group.closure_subset_iff {G : Type u_1} [Group G] {s : Set G} {t : Set G} (ht : IsSubgroup t) :

Group.closure s ⊆ t ↔ s ⊆ t

theorem AddGroup.closure_mono {G : Type u_1} [AddGroup G] {s : Set G} {t : Set G} (h : s ⊆ t) :

AddGroup.closure s ⊆ AddGroup.closure t

theorem Group.closure_mono {G : Type u_1} [Group G] {s : Set G} {t : Set G} (h : s ⊆ t) :

Group.closure s ⊆ Group.closure t

@[simp]

theorem AddGroup.closure_addSubgroup {G : Type u_1} [AddGroup G] {s : Set G} (hs : IsAddSubgroup s) :

AddGroup.closure s = s

@[simp]

theorem Group.closure_subgroup {G : Type u_1} [Group G] {s : Set G} (hs : IsSubgroup s) :

Group.closure s = s

theorem AddGroup.exists_list_of_mem_closure {G : Type u_1} [AddGroup G] {s : Set G} {a : G} (h : a ∈ AddGroup.closure s) :

∃ (l : List G), (∀ x ∈ l, x ∈ s ∨ -x ∈ s) ∧ l.sum = a

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 ∈ l, x ∈ s ∨ x⁻¹ ∈ s) ∧ l.prod = a

theorem AddGroup.image_closure {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {f : G → H} (hf : IsAddGroupHom f) (s : Set G) :

f '' AddGroup.closure s = AddGroup.closure (f '' s)

theorem Group.image_closure {G : Type u_1} {H : Type u_2} [Group G] [Group H] {f : G → H} (hf : IsGroupHom f) (s : Set G) :

f '' Group.closure s = Group.closure (f '' s)

theorem AddGroup.mclosure_subset {G : Type u_1} [AddGroup G] {s : Set G} :

AddMonoid.Closure s ⊆ AddGroup.closure s

theorem Group.mclosure_subset {G : Type u_1} [Group G] {s : Set G} :

Monoid.Closure s ⊆ Group.closure s

theorem AddGroup.mclosure_neg_subset {G : Type u_1} [AddGroup G] {s : Set G} :

AddMonoid.Closure (Neg.neg ⁻¹' s) ⊆ AddGroup.closure s

theorem Group.mclosure_inv_subset {G : Type u_1} [Group G] {s : Set G} :

Monoid.Closure (Inv.inv ⁻¹' s) ⊆ Group.closure s

theorem AddGroup.closure_eq_mclosure {G : Type u_1} [AddGroup G] {s : Set G} :

AddGroup.closure s = AddMonoid.Closure (s ∪ Neg.neg ⁻¹' s)

theorem Group.closure_eq_mclosure {G : Type u_1} [Group G] {s : Set G} :

Group.closure s = Monoid.Closure (s ∪ Inv.inv ⁻¹' s)

theorem AddGroup.mem_closure_union_iff {G : Type u_4} [AddCommGroup G] {s : Set G} {t : Set G} {x : G} :

x ∈ AddGroup.closure (s ∪ t) ↔ ∃ y ∈ AddGroup.closure s, ∃ z ∈ AddGroup.closure t, y + z = x

theorem Group.mem_closure_union_iff {G : Type u_4} [CommGroup G] {s : Set G} {t : Set G} {x : G} :

x ∈ Group.closure (s ∪ t) ↔ ∃ y ∈ Group.closure s, ∃ z ∈ Group.closure t, y * z = x

theorem IsAddSubgroup.trivial_eq_closure {G : Type u_1} [AddGroup G] :

IsAddSubgroup.trivial G = AddGroup.closure ∅

theorem IsSubgroup.trivial_eq_closure {G : Type u_1} [Group G] :

IsSubgroup.trivial G = Group.closure ∅

theorem Group.conjugatesOf_subset {G : Type u_1} [Group G] {t : Set G} (ht : IsNormalSubgroup t) {a : G} (h : a ∈ t) :

conjugatesOf a ⊆ t

theorem Group.conjugatesOfSet_subset' {G : Type u_1} [Group G] {s : Set G} {t : Set G} (ht : IsNormalSubgroup t) (h : s ⊆ t) :

Group.conjugatesOfSet s ⊆ t

def Group.normalClosure {G : Type u_1} [Group G] (s : 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

Group.normalClosure s = Group.closure (Group.conjugatesOfSet s)

Instances For

theorem Group.conjugatesOfSet_subset_normalClosure {G : Type u_1} {s : Set G} [Group G] :

Group.conjugatesOfSet s ⊆ Group.normalClosure s

theorem Group.subset_normalClosure {G : Type u_1} {s : Set G} [Group G] :

s ⊆ Group.normalClosure s

theorem Group.normalClosure.isSubgroup {G : Type u_1} [Group G] (s : Set G) :

IsSubgroup (Group.normalClosure s)

The normal closure of a set is a subgroup.

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

IsNormalSubgroup (Group.normalClosure s)

The normal closure of s is a normal subgroup.

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

Group.normalClosure s ⊆ t

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

theorem Group.normalClosure_subset_iff {G : Type u_1} [Group G] {s : Set G} {t : Set G} (ht : IsNormalSubgroup t) :

s ⊆ t ↔ Group.normalClosure s ⊆ t

theorem Group.normalClosure_mono {G : Type u_1} [Group G] {s : Set G} {t : Set G} :

s ⊆ t → Group.normalClosure s ⊆ Group.normalClosure t

def AddSubgroup.of {G : Type u_1} [AddGroup G] {s : Set G} (h : IsAddSubgroup s) :

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

Equations

AddSubgroup.of h = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

theorem AddSubgroup.of.proof_1 {G : Type u_1} [AddGroup G] {s : Set G} (h : IsAddSubgroup s) :

∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s

theorem AddSubgroup.of.proof_2 {G : Type u_1} [AddGroup G] {s : Set G} (h : IsAddSubgroup s) :

0 ∈ s

def Subgroup.of {G : Type u_1} [Group G] {s : Set G} (h : IsSubgroup s) :

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

Equations

Subgroup.of h = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

theorem AddSubgroup.isAddSubgroup {G : Type u_1} [AddGroup G] (K : AddSubgroup G) :

IsAddSubgroup ↑K

theorem Subgroup.isSubgroup {G : Type u_1} [Group G] (K : Subgroup G) :

IsSubgroup ↑K

theorem AddSubgroup.of_normal {G : Type u_1} [AddGroup G] (s : Set G) (h : IsAddSubgroup s) (n : IsNormalAddSubgroup s) :

(AddSubgroup.of h).Normal

theorem Subgroup.of_normal {G : Type u_1} [Group G] (s : Set G) (h : IsSubgroup s) (n : IsNormalSubgroup s) :

(Subgroup.of h).Normal