# Documentation

Mathlib.GroupTheory.Subgroup.Finite

# Subgroups #

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

## Tags #

subgroup, subgroups

instance AddSubgroup.instFintypeSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup {G : Type u_1} [inst : ] (K : ) [inst : DecidablePred fun x => x K] [inst : ] :
Fintype { x // x K }
Equations
• = let_fun this := inferInstance; this
instance Subgroup.instFintypeSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup {G : Type u_1} [inst : ] (K : ) [inst : DecidablePred fun x => x K] [inst : ] :
Fintype { x // x K }
Equations
• = let_fun this := inferInstance; this
instance AddSubgroup.instFiniteSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup {G : Type u_1} [inst : ] (K : ) [inst : ] :
Finite { x // x K }
Equations
Equations
instance Subgroup.instFiniteSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup {G : Type u_1} [inst : ] (K : ) [inst : ] :
Finite { x // x K }
Equations

### Conversion to/from Additive/Multiplicative#

theorem AddSubgroup.list_sum_mem {G : Type u_1} [inst : ] (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} [inst : ] (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_1} [inst : ] (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_1} [inst : ] (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} [inst : ] (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} [inst : ] (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_1} [inst : ] (K : ) {ι : Type u_2} {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_1} [inst : ] (K : ) {ι : Type u_2} {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} [inst : ] (K : ) {ι : Type u_2} {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} [inst : ] (K : ) {ι : Type u_2} {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} [inst : ] (H : ) (l : List { x // x H }) :
↑() = List.sum (List.map Subtype.val l)
@[simp]
theorem Subgroup.val_list_prod {G : Type u_1} [inst : ] (H : ) (l : List { x // x H }) :
↑() = List.prod (List.map Subtype.val l)
@[simp]
theorem AddSubgroup.val_multiset_sum {G : Type u_1} [inst : ] (H : ) (m : Multiset { x // x H }) :
↑() = Multiset.sum (Multiset.map Subtype.val m)
@[simp]
theorem Subgroup.val_multiset_prod {G : Type u_1} [inst : ] (H : ) (m : Multiset { x // x H }) :
↑() = Multiset.prod (Multiset.map Subtype.val m)
@[simp]
theorem AddSubgroup.val_finset_sum {ι : Type u_1} {G : Type u_2} [inst : ] (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_1} {G : Type u_2} [inst : ] (H : ) (f : ι{ x // x H }) (s : ) :
↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)
def AddSubgroup.fintypeBot.proof_1 {G : Type u_1} [inst : ] :
∀ (x : { x // x }), x {0}
Equations
instance AddSubgroup.fintypeBot {G : Type u_1} [inst : ] :
Fintype { x // x }
Equations
• AddSubgroup.fintypeBot = { elems := {0}, complete := (_ : ∀ (x : { x // x }), x {0}) }
instance Subgroup.fintypeBot {G : Type u_1} [inst : ] :
Fintype { x // x }
Equations
• Subgroup.fintypeBot = { elems := {1}, complete := (_ : ∀ (x : { x // x }), x {1}) }
abbrev AddSubgroup.card_bot.match_1 {G : Type u_1} [inst : ] (motive : { x // x }Prop) :
(x : { x // x }) → ((_y : G) → (hy : _y ) → motive { val := _y, property := hy }) → motive x
Equations
theorem AddSubgroup.card_bot {G : Type u_1} [inst : ] :
∀ {x : Fintype { x // x }}, Fintype.card { x // x } = 1
theorem Subgroup.card_bot {G : Type u_1} [inst : ] :
∀ {x : Fintype { x // x }}, Fintype.card { x // x } = 1
theorem AddSubgroup.eq_top_of_card_eq {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] [inst : ] (h : Fintype.card { x // x H } = ) :
H =
theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] [inst : ] (h : Fintype.card { x // x H } = ) :
H =
theorem AddSubgroup.eq_top_of_le_card {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] [inst : ] (h : Fintype.card { x // x H }) :
H =
theorem Subgroup.eq_top_of_le_card {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] [inst : ] (h : Fintype.card { x // x H }) :
H =
theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] (h : Fintype.card { x // x H } 1) :
H =
theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] (h : Fintype.card { x // x H } 1) :
H =
theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] (h : Fintype.card { x // x H } = 1) :
H =
theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] (h : Fintype.card { x // x H } = 1) :
H =
theorem AddSubgroup.card_le_one_iff_eq_bot {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] :
Fintype.card { x // x H } 1 H =
theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] :
Fintype.card { x // x H } 1 H =
theorem AddSubgroup.one_lt_card_iff_ne_bot {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] :
1 < Fintype.card { x // x H } H
theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [inst : ] (H : ) [inst : Fintype { x // x H }] :
1 < Fintype.card { x // x H } H
theorem AddSubgroup.pi_mem_of_single_mem_aux {η : Type u_1} {f : ηType u_2} [inst : (i : η) → AddGroup (f i)] [inst : ] (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_1} {f : ηType u_2} [inst : (i : η) → Group (f i)] [inst : ] (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_1} {f : ηType u_2} [inst : (i : η) → AddGroup (f i)] [inst : ] [inst : ] {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_1} {f : ηType u_2} [inst : (i : η) → Group (f i)] [inst : ] [inst : ] {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_1} {f : ηType u_2} [inst : (i : η) → AddGroup (f i)] [inst : ] [inst : ] {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_1} {f : ηType u_2} [inst : (i : η) → Group (f i)] [inst : ] [inst : ] {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} [inst : ] {S : Set G} [inst : Finite S] {x : G} (h : ∀ (n : G), n Sx * n * x⁻¹ S) :
instance AddMonoidHom.decidableMemRange {G : Type u_1} [inst : ] {N : Type u_2} [inst : ] (f : G →+ N) [inst : ] [inst : ] :
DecidablePred fun x =>
Equations
• = Fintype.decidableExistsFintype
instance MonoidHom.decidableMemRange {G : Type u_1} [inst : ] {N : Type u_2} [inst : ] (f : G →* N) [inst : ] [inst : ] :
DecidablePred fun x =>
Equations
• = Fintype.decidableExistsFintype
instance AddMonoidHom.fintypeMrange {M : Type u_1} {N : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (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.

Equations
instance MonoidHom.fintypeMrange {M : Type u_1} {N : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] (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.

Equations
instance AddMonoidHom.fintypeRange {G : Type u_1} [inst : ] {N : Type u_2} [inst : ] [inst : ] [inst : ] (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.

Equations
instance MonoidHom.fintypeRange {G : Type u_1} [inst : ] {N : Type u_2} [inst : ] [inst : ] [inst : ] (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.

Equations