# Documentation

Mathlib.GroupTheory.Subgroup.Finite

# Subgroups #

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

## Tags #

subgroup, subgroups

### Conversion to/from Additive/Multiplicative#

theorem AddSubgroup.list_sum_mem {G : Type u_1} [] (K : ) {l : List G} :
(∀ (x : G), x lx K) → 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} :
(∀ (x : G), x lx K) → 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 : ) :
(∀ (a : G), a ga 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 : ) :
(∀ (a : G), a ga 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 : Set.Pairwise {x | x g} AddCommute) :
(∀ (a : G), a ga K) → Multiset.noncommSum g comm K
theorem Subgroup.multiset_noncommProd_mem {G : Type u_1} [] (K : ) (g : ) (comm : Set.Pairwise {x | x g} Commute) :
(∀ (a : G), a ga K) → Multiset.noncommProd g comm K
theorem AddSubgroup.sum_mem {G : Type u_3} [] (K : ) {ι : Type u_4} {t : } {f : ιG} (h : ∀ (c : ι), c tf c K) :
(Finset.sum t fun c => 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 : ∀ (c : ι), c tf c K) :
(Finset.prod t fun c => 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 : Set.Pairwise t fun a b => AddCommute (f a) (f b)) :
(∀ (c : ι), c tf c K) → Finset.noncommSum t f comm K
theorem Subgroup.noncommProd_mem {G : Type u_1} [] (K : ) {ι : Type u_3} {t : } {f : ιG} (comm : Set.Pairwise t fun a b => Commute (f a) (f b)) :
(∀ (c : ι), c tf c K) → Finset.noncommProd t f comm K
@[simp]
theorem AddSubgroup.val_list_sum {G : Type u_1} [] (H : ) (l : List { x // x H }) :
↑() = List.sum (List.map Subtype.val l)
@[simp]
theorem Subgroup.val_list_prod {G : Type u_1} [] (H : ) (l : List { x // x H }) :
↑() = List.prod (List.map Subtype.val l)
@[simp]
theorem AddSubgroup.val_multiset_sum {G : Type u_3} [] (H : ) (m : Multiset { x // x H }) :
↑() = Multiset.sum (Multiset.map Subtype.val m)
@[simp]
theorem Subgroup.val_multiset_prod {G : Type u_3} [] (H : ) (m : Multiset { x // x H }) :
↑() = Multiset.prod (Multiset.map Subtype.val m)
@[simp]
theorem AddSubgroup.val_finset_sum {ι : Type u_3} {G : Type u_4} [] (H : ) (f : ι{ x // x H }) (s : ) :
↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)
@[simp]
theorem Subgroup.val_finset_prod {ι : Type u_3} {G : Type u_4} [] (H : ) (f : ι{ x // x H }) (s : ) :
↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)
theorem AddSubgroup.fintypeBot.proof_1 {G : Type u_1} [] :
∀ (x : { x // x }), x {0}
instance AddSubgroup.fintypeBot {G : Type u_1} [] :
Fintype { x // x }
instance Subgroup.fintypeBot {G : Type u_1} [] :
Fintype { x // x }
abbrev AddSubgroup.card_bot.match_1 {G : Type u_1} [] (motive : { x // x }Prop) :
(x : { x // x }) → ((_y : G) → (hy : _y ) → motive { val := _y, property := hy }) → motive x
Instances For
theorem AddSubgroup.card_bot {G : Type u_1} [] :
∀ {x : Fintype { x // x }}, Fintype.card { x // x } = 1
theorem Subgroup.card_bot {G : Type u_1} [] :
∀ {x : Fintype { x // x }}, Fintype.card { x // x } = 1
theorem AddSubgroup.card_top {G : Type u_1} [] [] :
Fintype.card { x // x } =
theorem Subgroup.card_top {G : Type u_1} [] [] :
Fintype.card { x // x } =
theorem AddSubgroup.eq_top_of_card_eq {G : Type u_1} [] (H : ) [Fintype { x // x H }] [] (h : Fintype.card { x // x H } = ) :
H =
theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [] (H : ) [Fintype { x // x H }] [] (h : Fintype.card { x // x H } = ) :
H =
@[simp]
theorem AddSubgroup.card_eq_iff_eq_top {G : Type u_1} [] (H : ) [Fintype { x // x H }] [] :
Fintype.card { x // x H } = H =
@[simp]
theorem Subgroup.card_eq_iff_eq_top {G : Type u_1} [] (H : ) [Fintype { x // x H }] [] :
Fintype.card { x // x H } = H =
theorem AddSubgroup.eq_top_of_le_card {G : Type u_1} [] (H : ) [Fintype { x // x H }] [] (h : Fintype.card { x // x H }) :
H =
theorem Subgroup.eq_top_of_le_card {G : Type u_1} [] (H : ) [Fintype { x // x H }] [] (h : Fintype.card { x // x H }) :
H =
theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [] (H : ) [Fintype { x // x H }] (h : Fintype.card { x // x H } 1) :
H =
theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [] (H : ) [Fintype { x // x H }] (h : Fintype.card { x // x H } 1) :
H =
theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [] (H : ) [Fintype { x // x H }] (h : Fintype.card { x // x H } = 1) :
H =
theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [] (H : ) [Fintype { x // x H }] (h : Fintype.card { x // x H } = 1) :
H =
theorem AddSubgroup.card_le_one_iff_eq_bot {G : Type u_1} [] (H : ) [Fintype { x // x H }] :
Fintype.card { x // x H } 1 H =
theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [] (H : ) [Fintype { x // x H }] :
Fintype.card { x // x H } 1 H =
theorem AddSubgroup.one_lt_card_iff_ne_bot {G : Type u_1} [] (H : ) [Fintype { x // x H }] :
1 < Fintype.card { x // x H } H
theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [] (H : ) [Fintype { x // x H }] :
1 < Fintype.card { x // x H } H
theorem AddSubgroup.card_le_card_addGroup {G : Type u_1} [] (H : ) [] [Fintype { x // x H }] :
Fintype.card { x // x H }
theorem Subgroup.card_le_card_group {G : Type u_1} [] (H : ) [] [Fintype { x // x H }] :
Fintype.card { x // x 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 : ∀ (i : η), ¬i Ix i = 0) (h2 : ∀ (i : η), i IPi.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 : ∀ (i : η), ¬i Ix i = 1) (h2 : ∀ (i : η), i IPi.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 : ∀ (n : G), n Sx * n * x⁻¹ S) :
instance AddMonoidHom.decidableMemRange {G : Type u_1} [] {N : Type u_3} [] (f : G →+ N) [] [] :
DecidablePred fun x =>
instance MonoidHom.decidableMemRange {G : Type u_1} [] {N : Type u_3} [] (f : G →* N) [] [] :
DecidablePred fun x =>
instance AddMonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [] [] [] [] (f : M →+ N) :
Fintype { x // }

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.

instance MonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [] [] [] [] (f : M →* N) :
Fintype { x // }

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.

instance AddMonoidHom.fintypeRange {G : Type u_1} [] {N : Type u_3} [] [] [] (f : G →+ N) :
Fintype { x // }

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.

instance MonoidHom.fintypeRange {G : Type u_1} [] {N : Type u_3} [] [] [] (f : G →* N) :
Fintype { x // }

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.