mathlib docs: deprecated.subgroup

source

@[class]

structure is_add_subgroup {A : Type u_3} [add_group A] (s : set A) :

Prop

to_is_add_submonoid : is_add_submonoid s
neg_mem : ∀ {a : A}, a ∈ s → -a ∈ s

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

Instances

source

@[class]

structure is_subgroup {G : Type u_1} [group G] (s : set G) :

Prop

to_is_submonoid : is_submonoid s
inv_mem : ∀ {a : G}, a ∈ s → a⁻¹ ∈ s

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

Instances

source

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

is_add_subgroup s

source

theorem additive.is_add_subgroup_iff {G : Type u_1} [group G] {s : set G} :

is_add_subgroup s ↔ is_subgroup s

source

theorem multiplicative.is_subgroup {A : Type u_3} [add_group A] (s : set A) [is_add_subgroup s] :

is_subgroup s

source

theorem multiplicative.is_subgroup_iff {A : Type u_3} [add_group A] {s : set A} :

is_subgroup s ↔ is_add_subgroup s

source

@[instance]

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

add_group ↥s

source

@[instance]

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

group ↥s

Equations

subtype.group = {mul := monoid.mul subtype.monoid, mul_assoc := _, one := monoid.one subtype.monoid, one_mul := _, mul_one := _, inv := λ (x : ↥s), ⟨(↑x)⁻¹, _⟩, mul_left_inv := _}

source

@[instance]

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

comm_group ↥s

Equations

subtype.comm_group = {mul := group.mul subtype.group, mul_assoc := _, one := group.one subtype.group, one_mul := _, mul_one := _, inv := group.inv subtype.group, mul_left_inv := _, mul_comm := _}

source

@[instance]

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

add_comm_group ↥s

source

@[simp]

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

↑-a = -↑a

source

@[simp]

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

↑a⁻¹ = (↑a)⁻¹

source

@[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

source

@[simp]

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

↑(n •ℤ a) = n •ℤ ↑a

source

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

is_subgroup s

source

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

is_add_subgroup s

source

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

is_add_subgroup s

source

@[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₂)

source

@[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₂)

source

@[instance]

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

is_subgroup (set.Inter s)

source

@[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)] :

is_add_subgroup (set.Inter s)

source

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)] (directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) :

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

source

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)] (directed : ∀ (i j : ι), ∃ (k : ι), s i ⊆ s k ∧ s j ⊆ s k) :

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

source

def gpowers {G : Type u_1} [group G] (x : G) :

set G

Equations

gpowers x = set.range (pow x)

source

def gmultiples {A : Type u_3} [add_group A] (x : A) :

set A

Equations

gmultiples x = set.range (λ (i : ℤ), i •ℤ x)

source

@[instance]

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

is_subgroup (gpowers x)

source

@[instance]

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

is_add_subgroup (gmultiples x)

source

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

source

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

source

theorem gpowers_subset {G : Type u_1} [group G] {a : G} {s : set G} [is_subgroup s] (h : a ∈ s) :

gpowers a ⊆ s

source

theorem gmultiples_subset {A : Type u_3} [add_group A] {a : A} {s : set A} [is_add_subgroup s] (h : a ∈ s) :

gmultiples a ⊆ s

source

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

a ∈ gpowers a

source

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

a ∈ gmultiples a

source

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

source

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

a⁻¹ ∈ s ↔ a ∈ s

source

theorem is_subgroup.mul_mem_cancel_right {G : Type u_1} {a b : G} [group G] (s : set G) [is_subgroup s] (h : a ∈ s) :

b * a ∈ s ↔ b ∈ s

source

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] (h : a ∈ s) :

b + a ∈ s ↔ b ∈ s

source

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] (h : a ∈ s) :

a + b ∈ s ↔ b ∈ s

source

theorem is_subgroup.mul_mem_cancel_left {G : Type u_1} {a b : G} [group G] (s : set G) [is_subgroup s] (h : a ∈ s) :

a * b ∈ s ↔ b ∈ s

source

theorem is_add_subgroup.sub_mem {A : Type u_1} [add_group A] (s : set A) [is_add_subgroup s] (a b : A) (ha : a ∈ s) (hb : b ∈ s) :

a - b ∈ s

source

@[class]

structure normal_add_subgroup {A : Type u_3} [add_group A] (s : set A) :

Prop

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

Instances

source

@[class]

structure normal_subgroup {G : Type u_1} [group G] (s : set G) :

Prop

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

Instances

source

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

normal_subgroup s

source

theorem normal_add_subgroup_of_add_comm_group {G : Type u_1} [add_comm_group G] (s : set G) [hs : is_add_subgroup s] :

normal_add_subgroup s

source

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

normal_add_subgroup s

source

theorem additive.normal_add_subgroup_iff {G : Type u_1} [group G] {s : set G} :

normal_add_subgroup s ↔ normal_subgroup s

source

theorem multiplicative.normal_subgroup {A : Type u_3} [add_group A] (s : set A) [normal_add_subgroup s] :

normal_subgroup s

source

theorem multiplicative.normal_subgroup_iff {A : Type u_3} [add_group A] {s : set A} :

normal_subgroup s ↔ normal_add_subgroup s

source

theorem is_subgroup.mem_norm_comm {G : Type u_1} [group G] {s : set G} [normal_subgroup s] {a b : G} (hab : a * b ∈ s) :

b * a ∈ s

source

theorem is_add_subgroup.mem_norm_comm {G : Type u_1} [add_group G] {s : set G} [normal_add_subgroup s] {a b : G} (hab : a + b ∈ s) :

b + a ∈ s

source

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

source

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

source

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

set G

source

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

set G

The trivial subgroup

Equations

is_subgroup.trivial G = {1}

source

@[simp]

theorem is_add_subgroup.mem_trivial {G : Type u_1} [add_group G] {g : G} :

g ∈ is_add_subgroup.trivial G ↔ g = 0

source

@[simp]

theorem is_subgroup.mem_trivial {G : Type u_1} [group G] {g : G} :

g ∈ is_subgroup.trivial G ↔ g = 1

source

@[instance]

def is_subgroup.trivial_normal {G : Type u_1} [group G] :

normal_subgroup (is_subgroup.trivial G)

source

@[instance]

def is_add_subgroup.trivial_normal {G : Type u_1} [add_group G] :

normal_add_subgroup (is_add_subgroup.trivial G)

source

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 ∈ s → x = 0

source

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 ∈ s → x = 1

source

@[instance]

def is_add_subgroup.univ_add_subgroup {G : Type u_1} [add_group G] :

normal_add_subgroup set.univ

source

@[instance]

def is_subgroup.univ_subgroup {G : Type u_1} [group G] :

normal_subgroup set.univ

source

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

set G

source

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

set G

Equations

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

source

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

source

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

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

source

@[instance]

def is_add_subgroup.add_center_normal {G : Type u_1} [add_group G] :

normal_add_subgroup (is_add_subgroup.add_center G)

source

@[instance]

def is_subgroup.center_normal {G : Type u_1} [group G] :

normal_subgroup (is_subgroup.center G)

source

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

set G

source

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

set G

Equations

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

source

@[instance]

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

is_subgroup (is_subgroup.normalizer s)

source

@[instance]

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

is_add_subgroup (is_add_subgroup.add_normalizer s)

source

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

s ⊆ is_subgroup.normalizer s

source

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

s ⊆ is_add_subgroup.add_normalizer s

source

@[instance]

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

normal_subgroup (subtype.val ⁻¹' s)

Every subgroup is a normal subgroup of its normalizer

source

@[instance]

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

normal_add_subgroup (subtype.val ⁻¹' s)

source

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

set G

Equations

is_group_hom.ker f = f ⁻¹' is_subgroup.trivial H

source

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

set G

source

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

x ∈ is_group_hom.ker f ↔ f x = 1

source

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

x ∈ is_add_group_hom.ker f ↔ f x = 0

source

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} (h : f (a + -b) = 0) :

f a = f b

source

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} (h : f (a * b⁻¹) = 1) :

f a = f b

source

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} (h : f (-a + b) = 0) :

f a = f b

source

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} (h : f (a⁻¹ * b) = 1) :

f a = f b

source

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} (h : f a = f b) :

f (a + -b) = 0

source

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} (h : f a = f b) :

f (a * b⁻¹) = 1

source

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} (h : f a = f b) :

f (-a + b) = 0

source

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} (h : f a = f b) :

f (a⁻¹ * b) = 1

source

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

source

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

source

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

source

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[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] :

is_add_subgroup (f '' s)

source

@[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] :

is_subgroup (f '' s)

source

@[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] :

is_add_subgroup (set.range f)

source

@[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] :

is_subgroup (set.range f)

source

@[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] :

is_subgroup (f ⁻¹' s)

source

@[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] :

is_add_subgroup (f ⁻¹' s)

source

@[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] :

normal_add_subgroup (f ⁻¹' s)

source

@[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] :

normal_subgroup (f ⁻¹' s)

source

@[instance]

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

normal_add_subgroup (is_add_group_hom.ker f)

source

@[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] :

normal_subgroup (is_group_hom.ker f)

source

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) [is_add_group_hom f] (h : is_add_group_hom.ker f = is_add_subgroup.trivial G) :

function.injective f

source

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] (h : is_group_hom.ker f = is_subgroup.trivial G) :

function.injective f

source

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) [is_add_group_hom f] (h : function.injective f) :

is_add_group_hom.ker f = is_add_subgroup.trivial G

source

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] (h : function.injective f) :

is_group_hom.ker f = is_subgroup.trivial G

source

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) [is_add_group_hom f] :

function.injective f ↔ is_add_group_hom.ker f = is_add_subgroup.trivial G

source

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

function.injective f ↔ is_group_hom.ker f = is_subgroup.trivial G

source

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 = 0 → x = 0

source

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 = 1 → x = 1

source

@[instance]

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

is_group_hom subtype.val

source

@[instance]

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

is_add_group_hom subtype.val

source

@[instance]

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

is_group_hom coe

source

@[instance]

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

is_add_group_hom coe

source

@[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, _⟩)

source

@[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, _⟩)

source

@[instance]

def set_inclusion.is_add_group_hom {G : Type u_1} [add_group G] {s t : set G} [is_add_subgroup s] [is_add_subgroup t] (h : s ⊆ t) :

is_add_group_hom (set.inclusion h)

source

@[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) :

is_group_hom (set.inclusion h)

source

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

↥(set.range ⇑f) →* H

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

Equations

f.range_subtype_val = monoid_hom.of subtype.val

source

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

↥(set.range ⇑f) →+ H

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

source

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

G →+ ↥(set.range ⇑f)

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

source

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

G →* ↥(set.range ⇑f)

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

Equations

f.range_factorization = {to_fun := set.range_factorization ⇑f, map_one' := _, map_mul' := _}

source

inductive add_group.in_closure {A : Type u_3} [add_group A] (s : set A) (a : A) :

Prop

basic : ∀ {A : Type u_3} [_inst_1 : add_group A] (s : set A) {a : A}, a ∈ s → add_group.in_closure s a
zero : ∀ {A : Type u_3} [_inst_1 : add_group A] (s : set A), add_group.in_closure s 0
neg : ∀ {A : Type u_3} [_inst_1 : add_group A] (s : set A) {a : A}, add_group.in_closure s a → add_group.in_closure s (-a)
add : ∀ {A : Type u_3} [_inst_1 : add_group A] (s : set A) {a b : A}, add_group.in_closure s a → add_group.in_closure s b → add_group.in_closure s (a + b)

source

inductive group.in_closure {G : Type u_1} [group G] (s : set G) (a : G) :

Prop

basic : ∀ {G : Type u_1} [_inst_1 : group G] (s : set G) {a : G}, a ∈ s → group.in_closure s a
one : ∀ {G : Type u_1} [_inst_1 : group G] (s : set G), group.in_closure s 1
inv : ∀ {G : Type u_1} [_inst_1 : group G] (s : set G) {a : G}, group.in_closure s a → group.in_closure s a⁻¹
mul : ∀ {G : Type u_1} [_inst_1 : group G] (s : set G) {a b : G}, group.in_closure s a → group.in_closure s b → group.in_closure s (a * b)

source

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

set G

source

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

set G

group.closure s is the subgroup closed over s, i.e. the smallest subgroup containg s.

Equations

group.closure s = {a : G | group.in_closure s a}

source

theorem add_group.mem_closure {G : Type u_1} [add_group G] {s : set G} {a : G} (a_1 : a ∈ s) :

a ∈ add_group.closure s

source

theorem group.mem_closure {G : Type u_1} [group G] {s : set G} {a : G} (a_1 : a ∈ s) :

a ∈ group.closure s

source

@[instance]

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

is_subgroup (group.closure s)

source

@[instance]

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

is_add_subgroup (add_group.closure s)

source

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

s ⊆ group.closure s

source

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

s ⊆ add_group.closure s

source

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

add_group.closure s ⊆ t

source

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

group.closure s ⊆ t

source

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

add_group.closure s ⊆ t ↔ s ⊆ t

source

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

group.closure s ⊆ t ↔ s ⊆ t

source

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

add_group.closure s ⊆ add_group.closure t

source

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

group.closure s ⊆ group.closure t

source

@[simp]

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

add_group.closure s = s

source

@[simp]

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

group.closure s = s

source

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

source

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

source

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

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

source

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

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

source

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

monoid.closure s ⊆ group.closure s

source

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

add_monoid.closure s ⊆ add_group.closure s

source

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

add_monoid.closure (has_neg.neg ⁻¹' s) ⊆ add_group.closure s

source

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

monoid.closure (has_inv.inv ⁻¹' s) ⊆ group.closure s

source

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

add_group.closure s = add_monoid.closure (s ∪ has_neg.neg ⁻¹' s)

source

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

group.closure s = monoid.closure (s ∪ has_inv.inv ⁻¹' s)

source

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

source

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

source

theorem add_group.gmultiples_eq_closure {G : Type u_1} [add_group G] {a : G} :

gmultiples a = add_group.closure {a}

source

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

gpowers a = group.closure {a}

source

theorem is_add_subgroup.trivial_eq_closure {G : Type u_1} [add_group G] :

is_add_subgroup.trivial G = add_group.closure ∅

source

theorem is_subgroup.trivial_eq_closure {G : Type u_1} [group G] :

is_subgroup.trivial G = group.closure ∅

source

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

group.conjugates a ⊆ t

source

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

group.conjugates_of_set s ⊆ t

source

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

group.normal_closure s = group.closure (group.conjugates_of_set s)

source

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

group.conjugates_of_set s ⊆ group.normal_closure s

source

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

s ⊆ group.normal_closure s

source

@[instance]

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

is_subgroup (group.normal_closure s)

The normal closure of a set is a subgroup.

source

@[instance]

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

normal_subgroup (group.normal_closure s)

The normal closure of s is a normal subgroup.

source

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

group.normal_closure s ⊆ t

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

source

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

s ⊆ t ↔ group.normal_closure s ⊆ t

source

theorem group.normal_closure_mono {G : Type u_1} [group G] {s t : set G} (a : s ⊆ t) :

group.normal_closure s ⊆ group.normal_closure t

source

@[class]

structure simple_group (G : Type u_4) [group G] :

Prop

simple : ∀ (N : set G) [_inst_1_1 : normal_subgroup N], N = is_subgroup.trivial G ∨ N = set.univ

Instances

multiplicative.simple_group

source

@[class]

structure simple_add_group (A : Type u_4) [add_group A] :

Prop

simple : ∀ (N : set A) [_inst_1_1 : normal_add_subgroup N], N = is_add_subgroup.trivial A ∨ N = set.univ

Instances

additive.simple_add_group

source

theorem additive.simple_add_group_iff {G : Type u_1} [group G] :

simple_add_group (additive G) ↔ simple_group G

source

@[instance]

def additive.simple_add_group {G : Type u_1} [group G] [simple_group G] :

simple_add_group (additive G)

source

theorem multiplicative.simple_group_iff {A : Type u_3} [add_group A] :

simple_group (multiplicative A) ↔ simple_add_group A

source

@[instance]

def multiplicative.simple_group {A : Type u_3} [add_group A] [simple_add_group A] :

simple_group (multiplicative A)

source

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] (hf : function.surjective f) :

simple_group H

source

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] (hf : function.surjective f) :

simple_add_group H

source

def subgroup.of {G : Type u_1} [group G] (s : set G) [h : is_subgroup s] :

subgroup G

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

Equations

subgroup.of s = {carrier := s, one_mem' := _, mul_mem' := _, inv_mem' := _}

source

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

add_subgroup G

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

source

@[instance]

def add_subgroup.is_add_subgroup {G : Type u_1} [add_group G] (K : add_subgroup G) :

is_add_subgroup ↑K

source

@[instance]

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

is_subgroup ↑K

source

@[instance]

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

(subgroup.of s).normal

source

@[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] :

(add_subgroup.of s).normal