Subgroups

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

Tags

subgroup, subgroups

instance Subgroup.instFintypeSubtypeMemOfDecidablePred {G : Type u_1} [Group G] (K : Subgroup G) [DecidablePred fun (x : G) => x ∈ K] [Fintype G] : Fintype ↥K

instance AddSubgroup.instFintypeSubtypeMemOfDecidablePred {G : Type u_1} [AddGroup G] (K : AddSubgroup G) [DecidablePred fun (x : G) => x ∈ K] [Fintype G] : Fintype ↥K

instance Subgroup.instFiniteSubtypeMem {G : Type u_1} [Group G] (K : Subgroup G) [Finite G] : Finite ↥K

instance AddSubgroup.instFiniteSubtypeMem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) [Finite G] : Finite ↥K

Conversion to/from Additive/Multiplicative

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

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

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

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

theorem Subgroup.multiset_prod_mem {G : Type u_3} [CommGroup G] (K : Subgroup G) (g : Multiset G) : (∀ a ∈ g, a ∈ K) → g.prod ∈ K

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

theorem AddSubgroup.multiset_sum_mem {G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) (g : Multiset G) : (∀ a ∈ g, a ∈ K) → g.sum ∈ K

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

theorem Subgroup.multiset_noncommProd_mem {G : Type u_1} [Group G] (K : Subgroup G) (g : Multiset G) (comm : {x : G | x ∈ g}.Pairwise Commute) : (∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K

theorem AddSubgroup.multiset_noncommSum_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (g : Multiset G) (comm : {x : G | x ∈ g}.Pairwise AddCommute) : (∀ a ∈ g, a ∈ K) → g.noncommSum comm ∈ K

theorem Subgroup.prod_mem {G : Type u_3} [CommGroup G] (K : Subgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) : ∏ c ∈ t, f c ∈ K

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

theorem AddSubgroup.sum_mem {G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) : ∑ c ∈ t, f c ∈ K

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

theorem Subgroup.noncommProd_mem {G : Type u_1} [Group G] (K : Subgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G} (comm : (↑t).Pairwise (Function.onFun Commute f)) : (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K

theorem AddSubgroup.noncommSum_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G} (comm : (↑t).Pairwise (Function.onFun AddCommute f)) : (∀ c ∈ t, f c ∈ K) → t.noncommSum f comm ∈ K

@[simp]

theorem Subgroup.val_list_prod {G : Type u_1} [Group G] (H : Subgroup G) (l : List ↥H) : ↑l.prod = (List.map Subtype.val l).prod

@[simp]

theorem AddSubgroup.val_list_sum {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (l : List ↥H) : ↑l.sum = (List.map Subtype.val l).sum

@[simp]

theorem Subgroup.val_multiset_prod {G : Type u_3} [CommGroup G] (H : Subgroup G) (m : Multiset ↥H) : ↑m.prod = (Multiset.map Subtype.val m).prod

@[simp]

theorem AddSubgroup.val_multiset_sum {G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) (m : Multiset ↥H) : ↑m.sum = (Multiset.map Subtype.val m).sum

@[simp]

theorem Subgroup.val_finset_prod {ι : Type u_3} {G : Type u_4} [CommGroup G] (H : Subgroup G) (f : ι → ↥H) (s : Finset ι) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

@[simp]

theorem AddSubgroup.val_finset_sum {ι : Type u_3} {G : Type u_4} [AddCommGroup G] (H : AddSubgroup G) (f : ι → ↥H) (s : Finset ι) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

instance Subgroup.fintypeBot {G : Type u_1} [Group G] : Fintype ↥⊥

instance AddSubgroup.fintypeBot {G : Type u_1} [AddGroup G] : Fintype ↥⊥

theorem Subgroup.card_bot {G : Type u_1} [Group G] : Nat.card ↥⊥ = 1

theorem AddSubgroup.card_bot {G : Type u_1} [AddGroup G] : Nat.card ↥⊥ = 1

theorem Subgroup.card_top {G : Type u_1} [Group G] : Nat.card ↥⊤ = Nat.card G

theorem AddSubgroup.card_top {G : Type u_1} [AddGroup G] : Nat.card ↥⊤ = Nat.card G

theorem Subgroup.eq_of_le_of_card_ge {G : Type u_1} [Group G] {H K : Subgroup G} [Finite ↥K] (hle : H ≤ K) (hcard : Nat.card ↥K ≤ Nat.card ↥H) : H = K

theorem AddSubgroup.eq_of_le_of_card_ge {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [Finite ↥K] (hle : H ≤ K) (hcard : Nat.card ↥K ≤ Nat.card ↥H) : H = K

theorem Subgroup.eq_top_of_le_card {G : Type u_1} [Group G] (H : Subgroup G) [Finite G] (h : Nat.card G ≤ Nat.card ↥H) : H = ⊤

theorem AddSubgroup.eq_top_of_le_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite G] (h : Nat.card G ≤ Nat.card ↥H) : H = ⊤

theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] (h : Nat.card ↥H = Nat.card G) : H = ⊤

theorem AddSubgroup.eq_top_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] (h : Nat.card ↥H = Nat.card G) : H = ⊤

@[simp]

theorem Subgroup.card_eq_iff_eq_top {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] : Nat.card ↥H = Nat.card G ↔ H = ⊤

@[simp]

theorem AddSubgroup.card_eq_iff_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] : Nat.card ↥H = Nat.card G ↔ H = ⊤

theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] (h : Nat.card ↥H ≤ 1) : H = ⊥

theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] (h : Nat.card ↥H ≤ 1) : H = ⊥

theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) (h : Nat.card ↥H = 1) : H = ⊥

theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (h : Nat.card ↥H = 1) : H = ⊥

theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] : Nat.card ↥H ≤ 1 ↔ H = ⊥

theorem AddSubgroup.card_le_one_iff_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] : Nat.card ↥H ≤ 1 ↔ H = ⊥

theorem Subgroup.eq_bot_iff_card {G : Type u_1} [Group G] (H : Subgroup G) : H = ⊥ ↔ Nat.card ↥H = 1

theorem AddSubgroup.eq_bot_iff_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H = ⊥ ↔ Nat.card ↥H = 1

theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] : 1 < Nat.card ↥H ↔ H ≠ ⊥

theorem AddSubgroup.one_lt_card_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] : 1 < Nat.card ↥H ↔ H ≠ ⊥

theorem Subgroup.card_le_card_group {G : Type u_1} [Group G] (H : Subgroup G) [Finite G] : Nat.card ↥H ≤ Nat.card G

theorem AddSubgroup.card_le_card_addGroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite G] : Nat.card ↥H ≤ Nat.card G

theorem Subgroup.card_le_of_le {G : Type u_1} [Group G] {H K : Subgroup G} [Finite ↥K] (h : H ≤ K) : Nat.card ↥H ≤ Nat.card ↥K

theorem AddSubgroup.card_le_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [Finite ↥K] (h : H ≤ K) : Nat.card ↥H ≤ Nat.card ↥K

theorem Subgroup.card_map_of_injective {G : Type u_1} [Group G] {H : Type u_3} [Group H] {K : Subgroup G} {f : G →* H} (hf : Function.Injective ⇑f) : Nat.card ↥(map f K) = Nat.card ↥K

theorem AddSubgroup.card_map_of_injective {G : Type u_1} [AddGroup G] {H : Type u_3} [AddGroup H] {K : AddSubgroup G} {f : G →+ H} (hf : Function.Injective ⇑f) : Nat.card ↥(map f K) = Nat.card ↥K

theorem Subgroup.card_subtype {G : Type u_1} [Group G] (K : Subgroup G) (L : Subgroup ↥K) : Nat.card ↥(map K.subtype L) = Nat.card ↥L

theorem AddSubgroup.card_subtype {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (L : AddSubgroup ↥K) : Nat.card ↥(map K.subtype L) = Nat.card ↥L

@[deprecated Submonoid.pi_mem_of_mulSingle_mem_aux (since := "2025-10-08")]

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 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) : x ∈ H

@[deprecated Submonoid.pi_mem_of_mulSingle_mem_aux (since := "2025-10-08")]

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 : ∀ i ∉ I, x i = 0) (h2 : ∀ i ∈ 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_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_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)} : pi Set.univ H ≤ J ↔ ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) ≤ J

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

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)} : pi Set.univ H ≤ J ↔ ∀ (i : η), 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.closure_pi {η : Type u_3} {f : η → Type u_4} [(i : η) → Group (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 1 ∈ s i) : closure (Set.univ.pi fun (i : η) => s i) = pi Set.univ fun (i : η) => closure (s i)

theorem AddSubgroup.closure_pi {η : Type u_3} {f : η → Type u_4} [(i : η) → AddGroup (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 0 ∈ s i) : closure (Set.univ.pi fun (i : η) => s i) = pi Set.univ fun (i : η) => closure (s i)

theorem Subgroup.mem_normalizer_fintype {G : Type u_1} [Group G] {S : Set G} [Finite ↑S] {x : G} (h : ∀ n ∈ S, x * n * x⁻¹ ∈ S) : x ∈ setNormalizer S

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 ∈ f.range

instance AddMonoidHom.decidableMemRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) [Fintype G] [DecidableEq N] : DecidablePred fun (x : N) => x ∈ f.range

instance MonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] (f : M →* N) : Fintype ↥(mrange f)

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.fintypeMrange {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] [Fintype M] [DecidableEq N] (f : M →+ N) : Fintype ↥(mrange f)

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.fintypeRange {G : Type u_1} [Group G] {N : Type u_3} [Group N] [Fintype G] [DecidableEq N] (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.

instance AddMonoidHom.fintypeRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] [Fintype G] [DecidableEq N] (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.

theorem Fintype.card_coeSort_mrange {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] {f : M →* N} (hf : Function.Injective ⇑f) : card ↥(MonoidHom.mrange f) = card M

theorem Fintype.card_coeSort_range {G : Type u_1} [Group G] {N : Type u_3} [Group N] [Fintype G] [DecidableEq N] {f : G →* N} (hf : Function.Injective ⇑f) : card ↥f.range = card G