# mathlib3documentation

group_theory.subgroup.finite

# Subgroups #

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

This file provides some result on multiplicative and additive subgroups in the finite context.

## Tags #

subgroup, subgroups

@[protected, instance]
def subgroup.fintype {G : Type u_1} [group G] (K : subgroup G) [d : decidable_pred (λ (_x : G), _x K)] [fintype G] :
Equations
@[protected, instance]
def add_subgroup.fintype {G : Type u_1} [add_group G] (K : add_subgroup G) [d : decidable_pred (λ (_x : G), _x K)] [fintype G] :
Equations
@[protected, instance]
def subgroup.finite {G : Type u_1} [group G] (K : subgroup G) [finite G] :
@[protected, instance]

@[protected]
theorem subgroup.list_prod_mem {G : Type u_1} [group G] (K : subgroup G) {l : list G} :
( (x : G), x l x K) l.prod K

Product of a list of elements in a subgroup is in the subgroup.

@[protected]
theorem add_subgroup.list_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {l : list G} :
( (x : G), x l x K) l.sum K

Sum of a list of elements in an add_subgroup is in the add_subgroup.

@[protected]
theorem add_subgroup.multiset_sum_mem {G : Type u_1} (K : add_subgroup G) (g : multiset G) :
( (a : G), a g a K) g.sum K

@[protected]
theorem subgroup.multiset_prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) (g : multiset G) :
( (a : G), a g a K) g.prod K

Product of a multiset of elements in a subgroup of a comm_group is in the subgroup.

theorem subgroup.multiset_noncomm_prod_mem {G : Type u_1} [group G] (K : subgroup G) (g : multiset G) (comm : {x : G | x g}.pairwise commute) :
( (a : G), a g a K) g.noncomm_prod comm K
theorem add_subgroup.multiset_noncomm_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) (g : multiset G) (comm : {x : G | x g}.pairwise add_commute) :
( (a : G), a g a K) g.noncomm_sum comm K
@[protected]
theorem add_subgroup.sum_mem {G : Type u_1} (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι G} (h : (c : ι), c t f c K) :
t.sum (λ (c : ι), f c) K

Sum of elements in an add_subgroup of an add_comm_group indexed by a finset is in the add_subgroup.

@[protected]
theorem subgroup.prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι G} (h : (c : ι), c t f c K) :
t.prod (λ (c : ι), f c) K

Product of elements of a subgroup of a comm_group indexed by a finset is in the subgroup.

theorem add_subgroup.noncomm_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι G} (comm : t.pairwise (λ (a b : ι), add_commute (f a) (f b))) :
( (c : ι), c t f c K) t.noncomm_sum f comm K
theorem subgroup.noncomm_prod_mem {G : Type u_1} [group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι G} (comm : t.pairwise (λ (a b : ι), commute (f a) (f b))) :
( (c : ι), c t f c K) t.noncomm_prod f comm K
@[simp, norm_cast]
theorem add_subgroup.coe_list_sum {G : Type u_1} [add_group G] (H : add_subgroup G) (l : list H) :
(l.sum) = l).sum
@[simp, norm_cast]
theorem subgroup.coe_list_prod {G : Type u_1} [group G] (H : subgroup G) (l : list H) :
(l.prod) = l).prod
@[simp, norm_cast]
theorem subgroup.coe_multiset_prod {G : Type u_1} [comm_group G] (H : subgroup G) (m : multiset H) :
(m.prod) = m).prod
@[simp, norm_cast]
theorem add_subgroup.coe_multiset_sum {G : Type u_1} (H : add_subgroup G) (m : multiset H) :
(m.sum) = m).sum
@[simp, norm_cast]
theorem add_subgroup.coe_finset_sum {ι : Type u_1} {G : Type u_2} (H : add_subgroup G) (f : ι H) (s : finset ι) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp, norm_cast]
theorem subgroup.coe_finset_prod {ι : Type u_1} {G : Type u_2} [comm_group G] (H : subgroup G) (f : ι H) (s : finset ι) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
@[protected, instance]
def subgroup.fintype_bot {G : Type u_1} [group G] :
Equations
@[protected, instance]
Equations
@[simp]
theorem subgroup.card_bot {G : Type u_1} [group G] {_x : fintype } :
@[simp]
theorem add_subgroup.card_bot {G : Type u_1} [add_group G] {_x : fintype } :
theorem subgroup.eq_top_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype H] [fintype G] (h : = ) :
H =
theorem add_subgroup.eq_top_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype H] [fintype G] (h : = ) :
H =
theorem subgroup.eq_top_of_le_card {G : Type u_1} [group G] (H : subgroup G) [fintype H] [fintype G] (h : ) :
H =
theorem add_subgroup.eq_top_of_le_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype H] [fintype G] (h : ) :
H =
theorem subgroup.eq_bot_of_card_le {G : Type u_1} [group G] (H : subgroup G) [fintype H] (h : 1) :
H =
theorem add_subgroup.eq_bot_of_card_le {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype H] (h : 1) :
H =
theorem add_subgroup.eq_bot_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype H] (h : = 1) :
H =
theorem subgroup.eq_bot_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype H] (h : = 1) :
H =
theorem subgroup.card_le_one_iff_eq_bot {G : Type u_1} [group G] (H : subgroup G) [fintype H] :
H =
theorem subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [group G] (H : subgroup G) [fintype H] :
theorem subgroup.pi_mem_of_mul_single_mem_aux {η : Type u_3} {f : η Type u_4} [Π (i : η), group (f i)] [decidable_eq η] (I : finset η) {H : subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h1 : (i : η), i I x i = 1) (h2 : (i : η), i I (x i) H) :
x H
theorem add_subgroup.pi_mem_of_single_mem_aux {η : Type u_3} {f : η Type u_4} [Π (i : η), add_group (f i)] [decidable_eq η] (I : finset η) {H : add_subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h1 : (i : η), i I x i = 0) (h2 : (i : η), i I (x i) H) :
x H
theorem add_subgroup.pi_mem_of_single_mem {η : Type u_3} {f : η Type u_4} [Π (i : η), add_group (f i)] [finite η] [decidable_eq η] {H : add_subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h : (i : η), (x i) H) :
x H
theorem subgroup.pi_mem_of_mul_single_mem {η : Type u_3} {f : η Type u_4} [Π (i : η), group (f i)] [finite η] [decidable_eq η] {H : subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h : (i : η), (x i) H) :
x H
theorem subgroup.pi_le_iff {η : Type u_3} {f : η Type u_4} [Π (i : η), group (f i)] [decidable_eq η] [finite η] {H : Π (i : η), subgroup (f i)} {J : subgroup (Π (i : η), f i)} :
(i : η), (H i) J

For finite index types, the subgroup.pi is generated by the embeddings of the groups.

theorem add_subgroup.pi_le_iff {η : Type u_3} {f : η Type u_4} [Π (i : η), add_group (f i)] [decidable_eq η] [finite η] {H : Π (i : η), add_subgroup (f i)} {J : add_subgroup (Π (i : η), f i)} :
(i : η), (H i) J

For finite index types, the subgroup.pi is generated by the embeddings of the additive groups.

theorem subgroup.mem_normalizer_fintype {G : Type u_1} [group G] {S : set G} [finite S] {x : G} (h : (n : G), n S x * n * x⁻¹ S) :
@[protected, instance]
def add_monoid_hom.decidable_mem_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) [fintype G] [decidable_eq N] :
decidable_pred (λ (_x : N), _x f.range)
Equations
@[protected, instance]
def monoid_hom.decidable_mem_range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) [fintype G] [decidable_eq N] :
decidable_pred (λ (_x : N), _x f.range)
Equations
@[protected, instance]
def add_monoid_hom.fintype_mrange {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] [fintype M] [decidable_eq N] (f : M →+ N) :

The range of a finite additive monoid under an additive monoid homomorphism is finite.

Note: this instance can form a diamond with subtype.fintype or subgroup.fintype in the presence of fintype N.

Equations
@[protected, instance]
def monoid_hom.fintype_mrange {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] [fintype M] [decidable_eq N] (f : M →* N) :

The range of a finite monoid under a monoid homomorphism is finite. Note: this instance can form a diamond with subtype.fintype in the presence of fintype N.

Equations
@[protected, instance]
def monoid_hom.fintype_range {G : Type u_1} [group G] {N : Type u_3} [group N] [fintype G] [decidable_eq N] (f : G →* N) :

The range of a finite group under a group homomorphism is finite.

Note: this instance can form a diamond with subtype.fintype or subgroup.fintype in the presence of fintype N.

Equations
@[protected, instance]
def add_monoid_hom.fintype_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] [fintype G] [decidable_eq N] (f : G →+ N) :

The range of a finite additive group under an additive group homomorphism is finite.

Note: this instance can form a diamond with subtype.fintype or subgroup.fintype in the presence of fintype N.

Equations