Documentation

Mathlib.GroupTheory.Subgroup.Finite

Subgroups #

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

Tags #

subgroup, subgroups

Equations

Conversion to/from Additive/Multiplicative #

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

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

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

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

theorem AddSubgroup.multiset_sum_mem {G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) (g : Multiset G) :
(ag, a K)Multiset.sum g 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} [CommGroup G] (K : Subgroup G) (g : Multiset G) :
(ag, a K)Multiset.prod g 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} [AddGroup G] (K : AddSubgroup G) (g : Multiset G) (comm : Set.Pairwise {x : G | x g} AddCommute) :
(ag, a K)Multiset.noncommSum g comm K
theorem Subgroup.multiset_noncommProd_mem {G : Type u_1} [Group G] (K : Subgroup G) (g : Multiset G) (comm : Set.Pairwise {x : G | x g} Commute) :
(ag, a K)Multiset.noncommProd g comm K
theorem AddSubgroup.sum_mem {G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) {ι : Type u_4} {t : Finset ι} {f : ιG} (h : ct, f 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} [CommGroup G] (K : Subgroup G) {ι : Type u_4} {t : Finset ι} {f : ιG} (h : ct, f 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} [AddGroup G] (K : AddSubgroup G) {ι : Type u_3} {t : Finset ι} {f : ιG} (comm : Set.Pairwise t fun (a b : ι) => AddCommute (f a) (f b)) :
(ct, f c K)Finset.noncommSum t f comm K
theorem Subgroup.noncommProd_mem {G : Type u_1} [Group G] (K : Subgroup G) {ι : Type u_3} {t : Finset ι} {f : ιG} (comm : Set.Pairwise t fun (a b : ι) => Commute (f a) (f b)) :
(ct, f c K)Finset.noncommProd t f comm K
@[simp]
theorem AddSubgroup.val_list_sum {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (l : List H) :
(List.sum l) = List.sum (List.map Subtype.val l)
@[simp]
theorem Subgroup.val_list_prod {G : Type u_1} [Group G] (H : Subgroup G) (l : List H) :
(List.prod l) = List.prod (List.map Subtype.val l)
@[simp]
theorem AddSubgroup.val_multiset_sum {G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) (m : Multiset H) :
(Multiset.sum m) = Multiset.sum (Multiset.map Subtype.val m)
@[simp]
theorem Subgroup.val_multiset_prod {G : Type u_3} [CommGroup G] (H : Subgroup G) (m : Multiset H) :
(Multiset.prod m) = Multiset.prod (Multiset.map Subtype.val m)
@[simp]
theorem AddSubgroup.val_finset_sum {ι : Type u_3} {G : Type u_4} [AddCommGroup G] (H : AddSubgroup G) (f : ιH) (s : Finset ι) :
(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} [CommGroup G] (H : Subgroup G) (f : ιH) (s : Finset ι) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (f i)
theorem AddSubgroup.fintypeBot.proof_1 {G : Type u_1} [AddGroup G] :
∀ (x : ), x {0}
instance AddSubgroup.fintypeBot {G : Type u_1} [AddGroup G] :
Equations
  • AddSubgroup.fintypeBot = { elems := {0}, complete := (_ : ∀ (x : ), x {0}) }
instance Subgroup.fintypeBot {G : Type u_1} [Group G] :
Equations
  • Subgroup.fintypeBot = { elems := {1}, complete := (_ : ∀ (x : ), x {1}) }
abbrev AddSubgroup.card_bot.match_1 {G : Type u_1} [AddGroup G] (motive : Prop) :
∀ (x : ), (∀ (_y : G) (hy : _y ), motive { val := _y, property := hy })motive x
Equations
  • (_ : motive x) = (_ : motive x)
Instances For
    theorem AddSubgroup.card_bot {G : Type u_1} [AddGroup G] :
    ∀ {x : Fintype }, Fintype.card = 1
    theorem Subgroup.card_bot {G : Type u_1} [Group G] :
    ∀ {x : Fintype }, Fintype.card = 1
    theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] [Fintype G] (h : Fintype.card H = Fintype.card G) :
    H =
    @[simp]
    @[simp]
    theorem Subgroup.card_eq_iff_eq_top {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] [Fintype G] :
    theorem Subgroup.eq_top_of_le_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] [Fintype G] (h : Fintype.card G Fintype.card H) :
    H =
    theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype H] (h : Fintype.card H 1) :
    H =
    theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] (h : Fintype.card H 1) :
    H =
    theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype H] (h : Fintype.card H = 1) :
    H =
    theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] (h : Fintype.card H = 1) :
    H =
    theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] :
    theorem AddSubgroup.eq_bot_iff_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype H] :
    theorem Subgroup.eq_bot_iff_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] :
    theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) [Fintype H] :
    theorem AddSubgroup.pi_mem_of_single_mem_aux {η : Type u_3} {f : ηType u_4} [(i : η) → AddGroup (f i)] [DecidableEq η] (I : Finset η) {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)] [DecidableEq η] (I : Finset η) {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)] [Finite η] [DecidableEq η] {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)] [Finite η] [DecidableEq η] {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)] [DecidableEq η] [Finite η] {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} :
    AddSubgroup.pi Set.univ H J ∀ (i : η), AddSubgroup.map (AddMonoidHom.single f i) (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)] [DecidableEq η] [Finite η] {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} :
    Subgroup.pi Set.univ H J ∀ (i : η), Subgroup.map (MonoidHom.single f i) (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} [Group G] {S : Set G} [Finite S] {x : G} (h : nS, x * n * x⁻¹ S) :
    instance AddMonoidHom.decidableMemRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) [Fintype G] [DecidableEq N] :
    Equations
    instance MonoidHom.decidableMemRange {G : Type u_1} [Group G] {N : Type u_3} [Group N] (f : G →* N) [Fintype G] [DecidableEq N] :
    DecidablePred fun (x : N) => x MonoidHom.range f
    Equations
    instance AddMonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] [Fintype M] [DecidableEq 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
    instance MonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] [Fintype M] [DecidableEq 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
    instance AddMonoidHom.fintypeRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] [Fintype G] [DecidableEq 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
    instance MonoidHom.fintypeRange {G : Type u_1} [Group G] {N : Type u_3} [Group N] [Fintype G] [DecidableEq 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