# Subgroups #

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

## Tags #

subgroup, subgroups

instance AddSubgroup.instFintypeSubtypeMemOfDecidablePred {G : Type u_1} [] (K : ) [DecidablePred fun (x : G) => x K] [] :
Fintype K
Equations
• K.instFintypeSubtypeMemOfDecidablePred = let_fun this := inferInstance; this
instance Subgroup.instFintypeSubtypeMemOfDecidablePred {G : Type u_1} [] (K : ) [DecidablePred fun (x : G) => x K] [] :
Fintype K
Equations
• K.instFintypeSubtypeMemOfDecidablePred = let_fun this := inferInstance; this
instance AddSubgroup.instFiniteSubtypeMem {G : Type u_1} [] (K : ) [] :
Finite K
Equations
• =
instance Subgroup.instFiniteSubtypeMem {G : Type u_1} [] (K : ) [] :
Finite K
Equations
• =

### Conversion to/from Additive/Multiplicative#

theorem AddSubgroup.list_sum_mem {G : Type u_1} [] (K : ) {l : List G} :
(xl, x K)l.sum K

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

theorem Subgroup.list_prod_mem {G : Type u_1} [] (K : ) {l : List G} :
(xl, x K)l.prod K

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

theorem AddSubgroup.multiset_sum_mem {G : Type u_3} [] (K : ) (g : ) :
(ag, a K)g.sum K

Sum of a multiset of elements in an AddSubgroup of an AddCommGroup is in the AddSubgroup.

theorem Subgroup.multiset_prod_mem {G : Type u_3} [] (K : ) (g : ) :
(ag, a K)g.prod K

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

theorem AddSubgroup.multiset_noncommSum_mem {G : Type u_1} [] (K : ) (g : ) (comm : {x : G | x g}.Pairwise AddCommute) :
(ag, a K)g.noncommSum comm K
theorem Subgroup.multiset_noncommProd_mem {G : Type u_1} [] (K : ) (g : ) (comm : {x : G | x g}.Pairwise Commute) :
(ag, a K)g.noncommProd comm K
theorem AddSubgroup.sum_mem {G : Type u_3} [] (K : ) {ι : Type u_4} {t : } {f : ιG} (h : ct, f c K) :
ct, f c K

Sum of elements in an AddSubgroup of an AddCommGroup indexed by a Finset is in the AddSubgroup.

theorem Subgroup.prod_mem {G : Type u_3} [] (K : ) {ι : Type u_4} {t : } {f : ιG} (h : ct, f c K) :
ct, f c K

Product of elements of a subgroup of a CommGroup indexed by a Finset is in the subgroup.

theorem AddSubgroup.noncommSum_mem {G : Type u_1} [] (K : ) {ι : Type u_3} {t : } {f : ιG} (comm : (t).Pairwise fun (a b : ι) => AddCommute (f a) (f b)) :
(ct, f c K)t.noncommSum f comm K
theorem Subgroup.noncommProd_mem {G : Type u_1} [] (K : ) {ι : Type u_3} {t : } {f : ιG} (comm : (t).Pairwise fun (a b : ι) => Commute (f a) (f b)) :
(ct, f c K)t.noncommProd f comm K
@[simp]
theorem AddSubgroup.val_list_sum {G : Type u_1} [] (H : ) (l : List H) :
l.sum = (List.map Subtype.val l).sum
@[simp]
theorem Subgroup.val_list_prod {G : Type u_1} [] (H : ) (l : List H) :
l.prod = (List.map Subtype.val l).prod
@[simp]
theorem AddSubgroup.val_multiset_sum {G : Type u_3} [] (H : ) (m : Multiset H) :
m.sum = (Multiset.map Subtype.val m).sum
@[simp]
theorem Subgroup.val_multiset_prod {G : Type u_3} [] (H : ) (m : Multiset H) :
m.prod = (Multiset.map Subtype.val m).prod
@[simp]
theorem AddSubgroup.val_finset_sum {ι : Type u_3} {G : Type u_4} [] (H : ) (f : ιH) (s : ) :
(is, f i) = is, (f i)
@[simp]
theorem Subgroup.val_finset_prod {ι : Type u_3} {G : Type u_4} [] (H : ) (f : ιH) (s : ) :
(is, f i) = is, (f i)
instance AddSubgroup.fintypeBot {G : Type u_1} [] :
Equations
• AddSubgroup.fintypeBot = { elems := {0}, complete := }
theorem AddSubgroup.fintypeBot.proof_1 {G : Type u_1} [] :
∀ (x : ), x {0}
instance Subgroup.fintypeBot {G : Type u_1} [] :
Equations
• Subgroup.fintypeBot = { elems := {1}, complete := }
theorem AddSubgroup.card_bot {G : Type u_1} [] :
= 1
theorem Subgroup.card_bot {G : Type u_1} [] :
= 1
theorem AddSubgroup.card_top {G : Type u_1} [] :
theorem Subgroup.card_top {G : Type u_1} [] :
theorem AddSubgroup.eq_top_of_card_eq {G : Type u_1} [] (H : ) [Finite H] (h : Nat.card H = ) :
H =
theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [] (H : ) [Finite H] (h : Nat.card H = ) :
H =
@[simp]
theorem AddSubgroup.card_eq_iff_eq_top {G : Type u_1} [] (H : ) [Finite H] :
Nat.card H = H =
@[simp]
theorem Subgroup.card_eq_iff_eq_top {G : Type u_1} [] (H : ) [Finite H] :
Nat.card H = H =
theorem AddSubgroup.eq_top_of_le_card {G : Type u_1} [] (H : ) [] (h : Nat.card H) :
H =
theorem Subgroup.eq_top_of_le_card {G : Type u_1} [] (H : ) [] (h : Nat.card H) :
H =
theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [] (H : ) [Finite H] (h : Nat.card H 1) :
H =
theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [] (H : ) [Finite H] (h : Nat.card H 1) :
H =
theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [] (H : ) (h : Nat.card H = 1) :
H =
theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [] (H : ) (h : Nat.card H = 1) :
H =
theorem AddSubgroup.card_le_one_iff_eq_bot {G : Type u_1} [] (H : ) [Finite H] :
Nat.card H 1 H =
theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [] (H : ) [Finite H] :
Nat.card H 1 H =
theorem AddSubgroup.eq_bot_iff_card {G : Type u_1} [] (H : ) :
H = Nat.card H = 1
theorem Subgroup.eq_bot_iff_card {G : Type u_1} [] (H : ) :
H = Nat.card H = 1
theorem AddSubgroup.one_lt_card_iff_ne_bot {G : Type u_1} [] (H : ) [Finite H] :
1 < Nat.card H H
theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [] (H : ) [Finite H] :
1 < Nat.card H H
theorem AddSubgroup.card_le_card_addGroup {G : Type u_1} [] (H : ) [] :
theorem Subgroup.card_le_card_group {G : Type u_1} [] (H : ) [] :
theorem AddSubgroup.pi_mem_of_single_mem_aux {η : Type u_3} {f : ηType u_4} [(i : η) → AddGroup (f i)] [] (I : ) {H : AddSubgroup ((i : η) → f i)} (x : (i : η) → f i) (h1 : iI, x i = 0) (h2 : iI, Pi.single i (x i) H) :
x H
theorem Subgroup.pi_mem_of_mulSingle_mem_aux {η : Type u_3} {f : ηType u_4} [(i : η) → Group (f i)] [] (I : ) {H : Subgroup ((i : η) → f i)} (x : (i : η) → f i) (h1 : iI, x i = 1) (h2 : iI, Pi.mulSingle i (x i) H) :
x H
theorem AddSubgroup.pi_mem_of_single_mem {η : Type u_3} {f : ηType u_4} [(i : η) → AddGroup (f i)] [] [] {H : AddSubgroup ((i : η) → f i)} (x : (i : η) → f i) (h : ∀ (i : η), Pi.single i (x i) H) :
x H
theorem Subgroup.pi_mem_of_mulSingle_mem {η : Type u_3} {f : ηType u_4} [(i : η) → Group (f i)] [] [] {H : Subgroup ((i : η) → f i)} (x : (i : η) → f i) (h : ∀ (i : η), Pi.mulSingle i (x i) H) :
x H
theorem AddSubgroup.pi_le_iff {η : Type u_3} {f : ηType u_4} [(i : η) → AddGroup (f i)] [] [] {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} :
AddSubgroup.pi Set.univ H J ∀ (i : η), AddSubgroup.map () (H i) J

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

theorem Subgroup.pi_le_iff {η : Type u_3} {f : ηType u_4} [(i : η) → Group (f i)] [] [] {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} :
Subgroup.pi Set.univ H J ∀ (i : η), Subgroup.map () (H i) J

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

theorem Subgroup.mem_normalizer_fintype {G : Type u_1} [] {S : Set G} [Finite S] {x : G} (h : nS, x * n * x⁻¹ S) :
instance AddMonoidHom.decidableMemRange {G : Type u_1} [] {N : Type u_3} [] (f : G →+ N) [] [] :
DecidablePred fun (x : N) => x f.range
Equations
• f.decidableMemRange x = Fintype.decidableExistsFintype
instance MonoidHom.decidableMemRange {G : Type u_1} [] {N : Type u_3} [] (f : G →* N) [] [] :
DecidablePred fun (x : N) => x f.range
Equations
• f.decidableMemRange x = Fintype.decidableExistsFintype
instance AddMonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [] [] [] [] (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
• f.fintypeMrange =
instance MonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [] [] [] [] (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
• f.fintypeMrange =
instance AddMonoidHom.fintypeRange {G : Type u_1} [] {N : Type u_3} [] [] [] (f : G →+ N) :
Fintype f.range

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
• f.fintypeRange =
instance MonoidHom.fintypeRange {G : Type u_1} [] {N : Type u_3} [] [] [] (f : G →* N) :
Fintype f.range

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
• f.fintypeRange =