Index of a Subgroup

In this file we define the index of a subgroup, and prove several divisibility properties. Several theorems proved in this file are known as Lagrange's theorem.

Main definitions

• H.index : the index of H : Subgroup G as a natural number, and returns 0 if the index is infinite.
• H.relIndex K : the relative index of H : Subgroup G in K : Subgroup G as a natural number, and returns 0 if the relative index is infinite.

Main results

• card_mul_index : Nat.card H * H.index = Nat.card G
• index_mul_card : H.index * Nat.card H = Nat.card G
• index_dvd_card : H.index ∣ Nat.card G
• relIndex_mul_index : If H ≤ K, then H.relindex K * K.index = H.index
• index_dvd_of_le : If H ≤ K, then K.index ∣ H.index
• relIndex_mul_relIndex : relIndex is multiplicative in towers
• MulAction.index_stabilizer: the index of the stabilizer is the cardinality of the orbit

theorem Subgroup.toSubmonoid_zpowers {G : Type u_1} [Group G] (g : G) : (zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹

theorem AddSubgroup.toAddSubmonoid_zmultiples {G : Type u_1} [AddGroup G] (g : G) : (zmultiples g).toAddSubmonoid = AddSubmonoid.multiples g ⊔ AddSubmonoid.multiples (-g)

theorem Submonoid.powers_le_zpowers {G : Type u_1} [Group G] (g : G) : powers g ≤ (Subgroup.zpowers g).toSubmonoid

theorem AddSubmonoid.multiples_le_zmultiples {G : Type u_1} [AddGroup G] (g : G) : multiples g ≤ (AddSubgroup.zmultiples g).toAddSubmonoid

noncomputable def Subgroup.index {G : Type u_1} [Group G] (H : Subgroup G) : ℕ

The index of a subgroup as a natural number. Returns 0 if the index is infinite.

Equations

• H.index = Nat.card (G ⧸ H)

noncomputable def AddSubgroup.index {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ℕ

The index of an additive subgroup as a natural number. Returns 0 if the index is infinite.

Equations

• H.index = Nat.card (G ⧸ H)

noncomputable def Subgroup.relIndex {G : Type u_1} [Group G] (H K : Subgroup G) : ℕ

If H and K are subgroups of a group G, then relIndex H K : ℕ is the index of H ∩ K in K. The function returns 0 if the index is infinite.

Equations

• H.relIndex K = (H.subgroupOf K).index

noncomputable def AddSubgroup.relIndex {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : ℕ

If H and K are subgroups of an additive group G, then relIndex H K : ℕ is the index of H ∩ K in K. The function returns 0 if the index is infinite.

Equations

• H.relIndex K = (H.addSubgroupOf K).index

@[deprecated Subgroup.relIndex (since := "2025-08-12")]

def Subgroup.relindex {G : Type u_1} [Group G] (H K : Subgroup G) : ℕ

Alias of Subgroup.relIndex.

---

If H and K are subgroups of a group G, then relIndex H K : ℕ is the index of H ∩ K in K. The function returns 0 if the index is infinite.

Equations

• @Subgroup.relindex = @Subgroup.relIndex

theorem Subgroup.index_comap_of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G' →* G} (hf : Function.Surjective ⇑f) : (comap f H).index = H.index

theorem AddSubgroup.index_comap_of_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G' →+ G} (hf : Function.Surjective ⇑f) : (comap f H).index = H.index

theorem Subgroup.index_comap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G' →* G) : (comap f H).index = H.relIndex f.range

theorem AddSubgroup.index_comap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G' →+ G) : (comap f H).index = H.relIndex f.range

theorem Subgroup.relIndex_comap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G' →* G) (K : Subgroup G') : (comap f H).relIndex K = H.relIndex (map f K)

theorem AddSubgroup.relIndex_comap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G' →+ G) (K : AddSubgroup G') : (comap f H).relIndex K = H.relIndex (map f K)

@[deprecated Subgroup.relIndex_comap (since := "2025-08-12")]

theorem Subgroup.relindex_comap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G' →* G) (K : Subgroup G') : (comap f H).relIndex K = H.relIndex (map f K)

Alias of Subgroup.relIndex_comap.

theorem Subgroup.relIndex_map_map_of_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (H K : Subgroup G) (hf : Function.Injective ⇑f) : (map f H).relIndex (map f K) = H.relIndex K

theorem AddSubgroup.relIndex_map_map_of_injective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (H K : AddSubgroup G) (hf : Function.Injective ⇑f) : (map f H).relIndex (map f K) = H.relIndex K

@[deprecated Subgroup.relIndex_map_map_of_injective (since := "2025-08-12")]

theorem Subgroup.relindex_map_map_of_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (H K : Subgroup G) (hf : Function.Injective ⇑f) : (map f H).relIndex (map f K) = H.relIndex K

Alias of Subgroup.relIndex_map_map_of_injective.

theorem Subgroup.relIndex_map_map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (H K : Subgroup G) : (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)

theorem AddSubgroup.relIndex_map_map {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H K : AddSubgroup G) : (map f H).relIndex (map f K) = (H ⊔ f.ker).relIndex (K ⊔ f.ker)

theorem Subgroup.relIndex_mul_index {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.relIndex K * K.index = H.index

theorem AddSubgroup.relIndex_mul_index {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : H.relIndex K * K.index = H.index

@[deprecated Subgroup.relIndex_mul_index (since := "2025-08-12")]

theorem Subgroup.relindex_mul_index {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.relIndex K * K.index = H.index

Alias of Subgroup.relIndex_mul_index.

theorem Subgroup.index_dvd_of_le {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : K.index ∣ H.index

theorem AddSubgroup.index_dvd_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : K.index ∣ H.index

theorem Subgroup.relIndex_dvd_index_of_le {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.relIndex K ∣ H.index

theorem AddSubgroup.relIndex_dvd_index_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : H.relIndex K ∣ H.index

@[deprecated Subgroup.relIndex_dvd_index_of_le (since := "2025-08-12")]

theorem Subgroup.relindex_dvd_index_of_le {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.relIndex K ∣ H.index

Alias of Subgroup.relIndex_dvd_index_of_le.

theorem Subgroup.relIndex_subgroupOf {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K ≤ L) : (H.subgroupOf L).relIndex (K.subgroupOf L) = H.relIndex K

theorem AddSubgroup.relIndex_addSubgroupOf {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hKL : K ≤ L) : (H.addSubgroupOf L).relIndex (K.addSubgroupOf L) = H.relIndex K

@[deprecated Subgroup.relIndex_subgroupOf (since := "2025-08-12")]

theorem Subgroup.relindex_subgroupOf {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K ≤ L) : (H.subgroupOf L).relIndex (K.subgroupOf L) = H.relIndex K

Alias of Subgroup.relIndex_subgroupOf.

theorem Subgroup.relIndex_mul_relIndex {G : Type u_1} [Group G] (H K L : Subgroup G) (hHK : H ≤ K) (hKL : K ≤ L) : H.relIndex K * K.relIndex L = H.relIndex L

theorem AddSubgroup.relIndex_mul_relIndex {G : Type u_1} [AddGroup G] (H K L : AddSubgroup G) (hHK : H ≤ K) (hKL : K ≤ L) : H.relIndex K * K.relIndex L = H.relIndex L

@[deprecated Subgroup.relIndex_mul_relIndex (since := "2025-08-12")]

theorem Subgroup.relindex_mul_relindex {G : Type u_1} [Group G] (H K L : Subgroup G) (hHK : H ≤ K) (hKL : K ≤ L) : H.relIndex K * K.relIndex L = H.relIndex L

Alias of Subgroup.relIndex_mul_relIndex.

theorem Subgroup.inf_relIndex_right {G : Type u_1} [Group G] (H K : Subgroup G) : (H ⊓ K).relIndex K = H.relIndex K

theorem AddSubgroup.inf_relIndex_right {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : (H ⊓ K).relIndex K = H.relIndex K

@[deprecated Subgroup.inf_relIndex_right (since := "2025-08-12")]

theorem Subgroup.inf_relindex_right {G : Type u_1} [Group G] (H K : Subgroup G) : (H ⊓ K).relIndex K = H.relIndex K

Alias of Subgroup.inf_relIndex_right.

theorem Subgroup.inf_relIndex_left {G : Type u_1} [Group G] (H K : Subgroup G) : (H ⊓ K).relIndex H = K.relIndex H

theorem AddSubgroup.inf_relIndex_left {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : (H ⊓ K).relIndex H = K.relIndex H

@[deprecated Subgroup.inf_relIndex_left (since := "2025-08-12")]

theorem Subgroup.inf_relindex_left {G : Type u_1} [Group G] (H K : Subgroup G) : (H ⊓ K).relIndex H = K.relIndex H

Alias of Subgroup.inf_relIndex_left.

theorem Subgroup.relIndex_inf_mul_relIndex {G : Type u_1} [Group G] (H K L : Subgroup G) : H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L

theorem AddSubgroup.relIndex_inf_mul_relIndex {G : Type u_1} [AddGroup G] (H K L : AddSubgroup G) : H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L

@[deprecated Subgroup.relIndex_inf_mul_relIndex (since := "2025-08-12")]

theorem Subgroup.relindex_inf_mul_relindex {G : Type u_1} [Group G] (H K L : Subgroup G) : H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L

Alias of Subgroup.relIndex_inf_mul_relIndex.

@[simp]

theorem Subgroup.relIndex_sup_right {G : Type u_1} [Group G] (H K : Subgroup G) [K.Normal] : K.relIndex (H ⊔ K) = K.relIndex H

@[simp]

theorem AddSubgroup.relIndex_sup_right {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.Normal] : K.relIndex (H ⊔ K) = K.relIndex H

@[deprecated Subgroup.relIndex_sup_right (since := "2025-08-12")]

theorem Subgroup.relindex_sup_right {G : Type u_1} [Group G] (H K : Subgroup G) [K.Normal] : K.relIndex (H ⊔ K) = K.relIndex H

Alias of Subgroup.relIndex_sup_right.

@[simp]

theorem Subgroup.relIndex_sup_left {G : Type u_1} [Group G] (H K : Subgroup G) [K.Normal] : K.relIndex (K ⊔ H) = K.relIndex H

@[simp]

theorem AddSubgroup.relIndex_sup_left {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.Normal] : K.relIndex (K ⊔ H) = K.relIndex H

@[deprecated Subgroup.relIndex_sup_left (since := "2025-08-12")]

theorem Subgroup.relindex_sup_left {G : Type u_1} [Group G] (H K : Subgroup G) [K.Normal] : K.relIndex (K ⊔ H) = K.relIndex H

Alias of Subgroup.relIndex_sup_left.

theorem Subgroup.relIndex_dvd_index_of_normal {G : Type u_1} [Group G] (H K : Subgroup G) [H.Normal] : H.relIndex K ∣ H.index

theorem AddSubgroup.relIndex_dvd_index_of_normal {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [H.Normal] : H.relIndex K ∣ H.index

@[deprecated Subgroup.relIndex_dvd_index_of_normal (since := "2025-08-12")]

theorem Subgroup.relindex_dvd_index_of_normal {G : Type u_1} [Group G] (H K : Subgroup G) [H.Normal] : H.relIndex K ∣ H.index

Alias of Subgroup.relIndex_dvd_index_of_normal.

theorem Subgroup.relIndex_dvd_of_le_left {G : Type u_1} [Group G] {H K : Subgroup G} (L : Subgroup G) (hHK : H ≤ K) : K.relIndex L ∣ H.relIndex L

theorem AddSubgroup.relIndex_dvd_of_le_left {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (L : AddSubgroup G) (hHK : H ≤ K) : K.relIndex L ∣ H.relIndex L

@[deprecated Subgroup.relIndex_dvd_of_le_left (since := "2025-08-12")]

theorem Subgroup.relindex_dvd_of_le_left {G : Type u_1} [Group G] {H K : Subgroup G} (L : Subgroup G) (hHK : H ≤ K) : K.relIndex L ∣ H.relIndex L

Alias of Subgroup.relIndex_dvd_of_le_left.

theorem Subgroup.index_eq_two_iff {G : Type u_1} [Group G] {H : Subgroup G} : H.index = 2 ↔ ∃ (a : G), ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)

A subgroup has index two if and only if there exists a such that for all b, exactly one of b * a and b belong to H.

theorem AddSubgroup.index_eq_two_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.index = 2 ↔ ∃ (a : G), ∀ (b : G), Xor' (b + a ∈ H) (b ∈ H)

An additive subgroup has index two if and only if there exists a such that for all b, exactly one of b + a and b belong to H.

theorem Subgroup.mul_mem_iff_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index = 2) {a b : G} : a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

theorem AddSubgroup.add_mem_iff_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index = 2) {a b : G} : a + b ∈ H ↔ (a ∈ H ↔ b ∈ H)

theorem Subgroup.mul_self_mem_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index = 2) (a : G) : a * a ∈ H

theorem AddSubgroup.add_self_mem_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index = 2) (a : G) : a + a ∈ H

theorem Subgroup.sq_mem_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index = 2) (a : G) : a ^ 2 ∈ H

theorem AddSubgroup.two_smul_mem_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index = 2) (a : G) : 2 • a ∈ H

@[simp]

theorem Subgroup.index_top {G : Type u_1} [Group G] : ⊤.index = 1

@[simp]

theorem AddSubgroup.index_top {G : Type u_1} [AddGroup G] : ⊤.index = 1

@[simp]

theorem Subgroup.index_bot {G : Type u_1} [Group G] : ⊥.index = Nat.card G

@[simp]

theorem AddSubgroup.index_bot {G : Type u_1} [AddGroup G] : ⊥.index = Nat.card G

@[simp]

theorem Subgroup.relIndex_top_left {G : Type u_1} [Group G] (H : Subgroup G) : ⊤.relIndex H = 1

@[simp]

theorem AddSubgroup.relIndex_top_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊤.relIndex H = 1

@[deprecated Subgroup.relIndex_top_left (since := "2025-08-12")]

theorem Subgroup.relindex_top_left {G : Type u_1} [Group G] (H : Subgroup G) : ⊤.relIndex H = 1

Alias of Subgroup.relIndex_top_left.

@[simp]

theorem Subgroup.relIndex_top_right {G : Type u_1} [Group G] (H : Subgroup G) : H.relIndex ⊤ = H.index

@[simp]

theorem AddSubgroup.relIndex_top_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.relIndex ⊤ = H.index

@[deprecated Subgroup.relIndex_top_right (since := "2025-08-12")]

theorem Subgroup.relindex_top_right {G : Type u_1} [Group G] (H : Subgroup G) : H.relIndex ⊤ = H.index

Alias of Subgroup.relIndex_top_right.

@[simp]

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

@[simp]

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

@[deprecated Subgroup.relIndex_bot_left (since := "2025-08-12")]

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

Alias of Subgroup.relIndex_bot_left.

@[simp]

theorem Subgroup.relIndex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) : H.relIndex ⊥ = 1

@[simp]

theorem AddSubgroup.relIndex_bot_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.relIndex ⊥ = 1

@[deprecated Subgroup.relIndex_bot_right (since := "2025-08-12")]

theorem Subgroup.relindex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) : H.relIndex ⊥ = 1

Alias of Subgroup.relIndex_bot_right.

@[simp]

theorem Subgroup.relIndex_self {G : Type u_1} [Group G] (H : Subgroup G) : H.relIndex H = 1

@[simp]

theorem AddSubgroup.relIndex_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.relIndex H = 1

@[deprecated Subgroup.relIndex_self (since := "2025-08-12")]

theorem Subgroup.relindex_self {G : Type u_1} [Group G] (H : Subgroup G) : H.relIndex H = 1

Alias of Subgroup.relIndex_self.

theorem Subgroup.index_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : f.ker.index = Nat.card ↥f.range

theorem AddSubgroup.index_ker {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') : f.ker.index = Nat.card ↥f.range

theorem Subgroup.relIndex_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (K : Subgroup G) (f : G →* G') : f.ker.relIndex K = Nat.card ↥(map f K)

theorem AddSubgroup.relIndex_ker {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (K : AddSubgroup G) (f : G →+ G') : f.ker.relIndex K = Nat.card ↥(map f K)

@[deprecated Subgroup.relIndex_ker (since := "2025-08-12")]

theorem Subgroup.relindex_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (K : Subgroup G) (f : G →* G') : f.ker.relIndex K = Nat.card ↥(map f K)

Alias of Subgroup.relIndex_ker.

@[simp]

theorem Subgroup.card_mul_index {G : Type u_1} [Group G] (H : Subgroup G) : Nat.card ↥H * H.index = Nat.card G

@[simp]

theorem AddSubgroup.card_mul_index {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nat.card ↥H * H.index = Nat.card G

theorem Subgroup.card_dvd_of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (hf : Function.Surjective ⇑f) : Nat.card G' ∣ Nat.card G

theorem AddSubgroup.card_dvd_of_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (hf : Function.Surjective ⇑f) : Nat.card G' ∣ Nat.card G

theorem Subgroup.card_range_dvd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : Nat.card ↥f.range ∣ Nat.card G

theorem AddSubgroup.card_range_dvd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') : Nat.card ↥f.range ∣ Nat.card G

theorem Subgroup.card_map_dvd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') : Nat.card ↥(map f H) ∣ Nat.card ↥H

theorem AddSubgroup.card_map_dvd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') : Nat.card ↥(map f H) ∣ Nat.card ↥H

theorem Subgroup.index_map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') : (map f H).index = (H ⊔ f.ker).index * f.range.index

theorem AddSubgroup.index_map {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') : (map f H).index = (H ⊔ f.ker).index * f.range.index

theorem Subgroup.index_map_dvd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : Function.Surjective ⇑f) : (map f H).index ∣ H.index

theorem AddSubgroup.index_map_dvd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : Function.Surjective ⇑f) : (map f H).index ∣ H.index

theorem Subgroup.dvd_index_map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : f.ker ≤ H) : H.index ∣ (map f H).index

theorem AddSubgroup.dvd_index_map {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : f.ker ≤ H) : H.index ∣ (map f H).index

theorem Subgroup.index_map_eq {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf1 : Function.Surjective ⇑f) (hf2 : f.ker ≤ H) : (map f H).index = H.index

theorem AddSubgroup.index_map_eq {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf1 : Function.Surjective ⇑f) (hf2 : f.ker ≤ H) : (map f H).index = H.index

theorem Subgroup.index_map_of_bijective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} (hf : Function.Bijective ⇑f) (H : Subgroup G) : (map f H).index = H.index

theorem AddSubgroup.index_map_of_bijective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (hf : Function.Bijective ⇑f) (H : AddSubgroup G) : (map f H).index = H.index

@[simp]

theorem Subgroup.index_map_equiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (e : G ≃* G') : (map (↑e) H).index = H.index

@[simp]

theorem AddSubgroup.index_map_equiv {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G') : (map (↑e) H).index = H.index

theorem Subgroup.index_map_of_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : Function.Injective ⇑f) : (map f H).index = H.index * f.range.index

theorem AddSubgroup.index_map_of_injective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : Function.Injective ⇑f) : (map f H).index = H.index * f.range.index

theorem Subgroup.index_map_subtype {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : (map H.subtype K).index = K.index * H.index

theorem AddSubgroup.index_map_subtype {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) : (map H.subtype K).index = K.index * H.index

theorem Subgroup.index_eq_card {G : Type u_1} [Group G] (H : Subgroup G) : H.index = Nat.card (G ⧸ H)

theorem AddSubgroup.index_eq_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.index = Nat.card (G ⧸ H)

theorem Subgroup.index_mul_card {G : Type u_1} [Group G] (H : Subgroup G) : H.index * Nat.card ↥H = Nat.card G

theorem AddSubgroup.index_mul_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.index * Nat.card ↥H = Nat.card G

theorem Subgroup.index_dvd_card {G : Type u_1} [Group G] (H : Subgroup G) : H.index ∣ Nat.card G

theorem AddSubgroup.index_dvd_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.index ∣ Nat.card G

theorem Subgroup.relIndex_dvd_card {G : Type u_1} [Group G] (H K : Subgroup G) : H.relIndex K ∣ Nat.card ↥K

theorem AddSubgroup.relIndex_dvd_card {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : H.relIndex K ∣ Nat.card ↥K

@[deprecated Subgroup.relIndex_dvd_card (since := "2025-08-12")]

theorem Subgroup.relindex_dvd_card {G : Type u_1} [Group G] (H K : Subgroup G) : H.relIndex K ∣ Nat.card ↥K

Alias of Subgroup.relIndex_dvd_card.

theorem Subgroup.relIndex_eq_zero_of_le_left {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H ≤ K) (hKL : K.relIndex L = 0) : H.relIndex L = 0

theorem AddSubgroup.relIndex_eq_zero_of_le_left {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hHK : H ≤ K) (hKL : K.relIndex L = 0) : H.relIndex L = 0

@[deprecated Subgroup.relIndex_eq_zero_of_le_left (since := "2025-08-12")]

theorem Subgroup.relindex_eq_zero_of_le_left {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H ≤ K) (hKL : K.relIndex L = 0) : H.relIndex L = 0

Alias of Subgroup.relIndex_eq_zero_of_le_left.

theorem Subgroup.relIndex_eq_zero_of_le_right {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K ≤ L) (hHK : H.relIndex K = 0) : H.relIndex L = 0

theorem AddSubgroup.relIndex_eq_zero_of_le_right {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hKL : K ≤ L) (hHK : H.relIndex K = 0) : H.relIndex L = 0

@[deprecated Subgroup.relIndex_eq_zero_of_le_right (since := "2025-08-12")]

theorem Subgroup.relindex_eq_zero_of_le_right {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K ≤ L) (hHK : H.relIndex K = 0) : H.relIndex L = 0

Alias of Subgroup.relIndex_eq_zero_of_le_right.

theorem Subgroup.relIndex_comap_ne_zero {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') {J K : Subgroup G'} (hJK : J.relIndex K ≠ 0) : (comap f J).relIndex (comap f K) ≠ 0

If J has finite index in K, then the same holds for their comaps under any group hom.

theorem AddSubgroup.relIndex_comap_ne_zero {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') {J K : AddSubgroup G'} (hJK : J.relIndex K ≠ 0) : (comap f J).relIndex (comap f K) ≠ 0

If J has finite index in K, then the same holds for their comaps under any additive group hom.

@[deprecated Subgroup.relIndex_comap_ne_zero (since := "2025-08-12")]

theorem Subgroup.relindex_comap_ne_zero {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') {J K : Subgroup G'} (hJK : J.relIndex K ≠ 0) : (comap f J).relIndex (comap f K) ≠ 0

Alias of Subgroup.relIndex_comap_ne_zero.

---

If J has finite index in K, then the same holds for their comaps under any group hom.

theorem Subgroup.index_eq_zero_of_relIndex_eq_zero {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relIndex K = 0) : H.index = 0

theorem AddSubgroup.index_eq_zero_of_relIndex_eq_zero {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H.relIndex K = 0) : H.index = 0

@[deprecated Subgroup.index_eq_zero_of_relIndex_eq_zero (since := "2025-08-12")]

theorem Subgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relIndex K = 0) : H.index = 0

Alias of Subgroup.index_eq_zero_of_relIndex_eq_zero.

theorem Subgroup.relIndex_le_of_le_left {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H ≤ K) (hHL : H.relIndex L ≠ 0) : K.relIndex L ≤ H.relIndex L

theorem AddSubgroup.relIndex_le_of_le_left {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hHK : H ≤ K) (hHL : H.relIndex L ≠ 0) : K.relIndex L ≤ H.relIndex L

@[deprecated Subgroup.relIndex_le_of_le_left (since := "2025-08-12")]

theorem Subgroup.relindex_le_of_le_left {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H ≤ K) (hHL : H.relIndex L ≠ 0) : K.relIndex L ≤ H.relIndex L

Alias of Subgroup.relIndex_le_of_le_left.

theorem Subgroup.relIndex_le_of_le_right {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K ≤ L) (hHL : H.relIndex L ≠ 0) : H.relIndex K ≤ H.relIndex L

theorem AddSubgroup.relIndex_le_of_le_right {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hKL : K ≤ L) (hHL : H.relIndex L ≠ 0) : H.relIndex K ≤ H.relIndex L

@[deprecated Subgroup.relIndex_le_of_le_right (since := "2025-08-12")]

theorem Subgroup.relindex_le_of_le_right {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K ≤ L) (hHL : H.relIndex L ≠ 0) : H.relIndex K ≤ H.relIndex L

Alias of Subgroup.relIndex_le_of_le_right.

theorem Subgroup.relIndex_ne_zero_trans {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H.relIndex K ≠ 0) (hKL : K.relIndex L ≠ 0) : H.relIndex L ≠ 0

theorem AddSubgroup.relIndex_ne_zero_trans {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hHK : H.relIndex K ≠ 0) (hKL : K.relIndex L ≠ 0) : H.relIndex L ≠ 0

@[deprecated Subgroup.relIndex_ne_zero_trans (since := "2025-08-12")]

theorem Subgroup.relindex_ne_zero_trans {G : Type u_1} [Group G] {H K L : Subgroup G} (hHK : H.relIndex K ≠ 0) (hKL : K.relIndex L ≠ 0) : H.relIndex L ≠ 0

Alias of Subgroup.relIndex_ne_zero_trans.

theorem Subgroup.relIndex_inf_ne_zero {G : Type u_1} [Group G] {H K L : Subgroup G} (hH : H.relIndex L ≠ 0) (hK : K.relIndex L ≠ 0) : (H ⊓ K).relIndex L ≠ 0

theorem AddSubgroup.relIndex_inf_ne_zero {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hH : H.relIndex L ≠ 0) (hK : K.relIndex L ≠ 0) : (H ⊓ K).relIndex L ≠ 0

@[deprecated Subgroup.relIndex_inf_ne_zero (since := "2025-08-12")]

theorem Subgroup.relindex_inf_ne_zero {G : Type u_1} [Group G] {H K L : Subgroup G} (hH : H.relIndex L ≠ 0) (hK : K.relIndex L ≠ 0) : (H ⊓ K).relIndex L ≠ 0

Alias of Subgroup.relIndex_inf_ne_zero.

theorem Subgroup.index_inf_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0

theorem AddSubgroup.index_inf_ne_zero {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0

theorem Subgroup.relIndex_inter_ne_zero {G : Type u_1} [Group G] {J K : Subgroup G} (hJK : J.relIndex K ≠ 0) (L : Subgroup G) : (J ⊓ L).relIndex (K ⊓ L) ≠ 0

If J has finite index in K, then J ⊓ L has finite index in K ⊓ L for any L.

theorem AddSubgroup.relIndex_inter_ne_zero {G : Type u_1} [AddGroup G] {J K : AddSubgroup G} (hJK : J.relIndex K ≠ 0) (L : AddSubgroup G) : (J ⊓ L).relIndex (K ⊓ L) ≠ 0

If J has finite index in K, then J ⊓ L has finite index in K ⊓ L for any L.

@[deprecated Subgroup.relIndex_inter_ne_zero (since := "2025-08-12")]

theorem Subgroup.relindex_inter_ne_zero {G : Type u_1} [Group G] {J K : Subgroup G} (hJK : J.relIndex K ≠ 0) (L : Subgroup G) : (J ⊓ L).relIndex (K ⊓ L) ≠ 0

Alias of Subgroup.relIndex_inter_ne_zero.

---

If J has finite index in K, then J ⊓ L has finite index in K ⊓ L for any L.

theorem Subgroup.relIndex_inf_le {G : Type u_1} [Group G] {H K L : Subgroup G} : (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

theorem AddSubgroup.relIndex_inf_le {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} : (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

@[deprecated Subgroup.relIndex_inf_le (since := "2025-08-12")]

theorem Subgroup.relindex_inf_le {G : Type u_1} [Group G] {H K L : Subgroup G} : (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L

Alias of Subgroup.relIndex_inf_le.

theorem Subgroup.index_inf_le {G : Type u_1} [Group G] {H K : Subgroup G} : (H ⊓ K).index ≤ H.index * K.index

theorem AddSubgroup.index_inf_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : (H ⊓ K).index ≤ H.index * K.index

theorem Subgroup.relIndex_iInf_ne_zero {G : Type u_1} [Group G] {L : Subgroup G} {ι : Type u_3} [_hι : Finite ι] {f : ι → Subgroup G} (hf : ∀ (i : ι), (f i).relIndex L ≠ 0) : (⨅ (i : ι), f i).relIndex L ≠ 0

theorem AddSubgroup.relIndex_iInf_ne_zero {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_3} [_hι : Finite ι] {f : ι → AddSubgroup G} (hf : ∀ (i : ι), (f i).relIndex L ≠ 0) : (⨅ (i : ι), f i).relIndex L ≠ 0

@[deprecated Subgroup.relIndex_iInf_ne_zero (since := "2025-08-12")]

theorem Subgroup.relindex_iInf_ne_zero {G : Type u_1} [Group G] {L : Subgroup G} {ι : Type u_3} [_hι : Finite ι] {f : ι → Subgroup G} (hf : ∀ (i : ι), (f i).relIndex L ≠ 0) : (⨅ (i : ι), f i).relIndex L ≠ 0

Alias of Subgroup.relIndex_iInf_ne_zero.

theorem Subgroup.relIndex_iInf_le {G : Type u_1} [Group G] {L : Subgroup G} {ι : Type u_3} [Fintype ι] (f : ι → Subgroup G) : (⨅ (i : ι), f i).relIndex L ≤ ∏ i : ι, (f i).relIndex L

theorem AddSubgroup.relIndex_iInf_le {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_3} [Fintype ι] (f : ι → AddSubgroup G) : (⨅ (i : ι), f i).relIndex L ≤ ∏ i : ι, (f i).relIndex L

@[deprecated Subgroup.relIndex_iInf_le (since := "2025-08-12")]

theorem Subgroup.relindex_iInf_le {G : Type u_1} [Group G] {L : Subgroup G} {ι : Type u_3} [Fintype ι] (f : ι → Subgroup G) : (⨅ (i : ι), f i).relIndex L ≤ ∏ i : ι, (f i).relIndex L

Alias of Subgroup.relIndex_iInf_le.

theorem Subgroup.index_iInf_ne_zero {G : Type u_1} [Group G] {ι : Type u_3} [Finite ι] {f : ι → Subgroup G} (hf : ∀ (i : ι), (f i).index ≠ 0) : (⨅ (i : ι), f i).index ≠ 0

theorem AddSubgroup.index_iInf_ne_zero {G : Type u_1} [AddGroup G] {ι : Type u_3} [Finite ι] {f : ι → AddSubgroup G} (hf : ∀ (i : ι), (f i).index ≠ 0) : (⨅ (i : ι), f i).index ≠ 0

theorem Subgroup.index_iInf_le {G : Type u_1} [Group G] {ι : Type u_3} [Fintype ι] (f : ι → Subgroup G) : (⨅ (i : ι), f i).index ≤ ∏ i : ι, (f i).index

theorem AddSubgroup.index_iInf_le {G : Type u_1} [AddGroup G] {ι : Type u_3} [Fintype ι] (f : ι → AddSubgroup G) : (⨅ (i : ι), f i).index ≤ ∏ i : ι, (f i).index

@[simp]

theorem Subgroup.index_eq_one {G : Type u_1} [Group G] {H : Subgroup G} : H.index = 1 ↔ H = ⊤

@[simp]

theorem AddSubgroup.index_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.index = 1 ↔ H = ⊤

@[simp]

theorem Subgroup.relIndex_eq_one {G : Type u_1} [Group G] {H K : Subgroup G} : H.relIndex K = 1 ↔ K ≤ H

@[simp]

theorem AddSubgroup.relIndex_eq_one {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.relIndex K = 1 ↔ K ≤ H

@[deprecated Subgroup.relIndex_eq_one (since := "2025-08-12")]

theorem Subgroup.relindex_eq_one {G : Type u_1} [Group G] {H K : Subgroup G} : H.relIndex K = 1 ↔ K ≤ H

Alias of Subgroup.relIndex_eq_one.

@[simp]

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

@[simp]

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

theorem Subgroup.inf_eq_bot_of_coprime {G : Type u_1} [Group G] {H K : Subgroup G} (h : (Nat.card ↥H).Coprime (Nat.card ↥K)) : H ⊓ K = ⊥

theorem AddSubgroup.inf_eq_bot_of_coprime {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : (Nat.card ↥H).Coprime (Nat.card ↥K)) : H ⊓ K = ⊥

theorem Subgroup.index_ne_zero_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [hH : Finite (G ⧸ H)] : H.index ≠ 0

theorem AddSubgroup.index_ne_zero_of_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : Finite (G ⧸ H)] : H.index ≠ 0

noncomputable def Subgroup.fintypeOfIndexNeZero {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.index ≠ 0) : Fintype (G ⧸ H)

Finite index implies finite quotient.

Equations

• Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)

noncomputable def AddSubgroup.fintypeOfIndexNeZero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.index ≠ 0) : Fintype (G ⧸ H)

Finite index implies finite quotient.

Equations

• AddSubgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)

theorem Subgroup.index_eq_zero_iff_infinite {G : Type u_1} [Group G] {H : Subgroup G} : H.index = 0 ↔ Infinite (G ⧸ H)

theorem AddSubgroup.index_eq_zero_iff_infinite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.index = 0 ↔ Infinite (G ⧸ H)

theorem Subgroup.index_ne_zero_iff_finite {G : Type u_1} [Group G] {H : Subgroup G} : H.index ≠ 0 ↔ Finite (G ⧸ H)

theorem AddSubgroup.index_ne_zero_iff_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.index ≠ 0 ↔ Finite (G ⧸ H)

theorem Subgroup.one_lt_index_of_ne_top {G : Type u_1} [Group G] {H : Subgroup G} [Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index

theorem AddSubgroup.one_lt_index_of_ne_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < H.index

theorem Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {X : Type u_3} [MulAction G X] [Finite (MulAction.orbitRel.Quotient G X)] (hi : H.index ≠ 0) : Finite (MulAction.orbitRel.Quotient (↥H) X)

theorem AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {X : Type u_3} [AddAction G X] [Finite (AddAction.orbitRel.Quotient G X)] (hi : H.index ≠ 0) : Finite (AddAction.orbitRel.Quotient (↥H) X)

theorem Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {X : Type u_3} [MulAction G X] [MulAction.IsPretransitive G X] (hi : H.index ≠ 0) : Finite (MulAction.orbitRel.Quotient (↥H) X)

theorem AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {X : Type u_3} [AddAction G X] [AddAction.IsPretransitive G X] (hi : H.index ≠ 0) : Finite (AddAction.orbitRel.Quotient (↥H) X)

theorem Subgroup.exists_pow_mem_of_index_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index ≠ 0) (a : G) : ∃ (n : ℕ), 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

theorem AddSubgroup.exists_nsmul_mem_of_index_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index ≠ 0) (a : G) : ∃ (n : ℕ), 0 < n ∧ n ≤ H.index ∧ n • a ∈ H

theorem Subgroup.exists_pow_mem_of_relIndex_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) : ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

theorem AddSubgroup.exists_nsmul_mem_of_relIndex_ne_zero {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) : ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ n • a ∈ H ⊓ K

@[deprecated Subgroup.exists_pow_mem_of_relIndex_ne_zero (since := "2025-08-12")]

theorem Subgroup.exists_pow_mem_of_relindex_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) : ∃ (n : ℕ), 0 < n ∧ n ≤ H.relIndex K ∧ a ^ n ∈ H ⊓ K

Alias of Subgroup.exists_pow_mem_of_relIndex_ne_zero.

theorem Subgroup.pow_mem_of_index_ne_zero_of_dvd {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index ≠ 0) (a : G) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n) : a ^ n ∈ H

theorem AddSubgroup.nsmul_mem_of_index_ne_zero_of_dvd {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index ≠ 0) (a : G) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n) : n • a ∈ H

theorem Subgroup.pow_mem_of_relIndex_ne_zero_of_dvd {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n) : a ^ n ∈ H ⊓ K

theorem AddSubgroup.nsmul_mem_of_relIndex_ne_zero_of_dvd {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n) : n • a ∈ H ⊓ K

@[deprecated Subgroup.pow_mem_of_relIndex_ne_zero_of_dvd (since := "2025-08-12")]

theorem Subgroup.pow_mem_of_relindex_ne_zero_of_dvd {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relIndex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n) : a ^ n ∈ H ⊓ K

Alias of Subgroup.pow_mem_of_relIndex_ne_zero_of_dvd.

@[simp]

theorem Subgroup.index_prod {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (K : Subgroup G') : (H.prod K).index = H.index * K.index

@[simp]

theorem AddSubgroup.index_prod {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (K : AddSubgroup G') : (H.prod K).index = H.index * K.index

@[deprecated AddSubgroup.index_prod (since := "2025-03-11")]

theorem AddSubgroup.index_sum {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (K : AddSubgroup G') : (H.prod K).index = H.index * K.index

Alias of AddSubgroup.index_prod.

@[simp]

theorem Subgroup.index_pi {G : Type u_1} [Group G] {ι : Type u_3} [Fintype ι] (H : ι → Subgroup G) : (pi Set.univ H).index = ∏ i : ι, (H i).index

@[simp]

theorem AddSubgroup.index_pi {G : Type u_1} [AddGroup G] {ι : Type u_3} [Fintype ι] (H : ι → AddSubgroup G) : (pi Set.univ H).index = ∏ i : ι, (H i).index

@[simp]

theorem Subgroup.index_toAddSubgroup {G : Type u_1} [Group G] {H : Subgroup G} : (toAddSubgroup H).index = H.index

@[simp]

theorem AddSubgroup.index_toSubgroup {G : Type u_3} [AddGroup G] (H : AddSubgroup G) : (toSubgroup H).index = H.index

@[simp]

theorem Subgroup.relIndex_toAddSubgroup {G : Type u_1} [Group G] {H K : Subgroup G} : (toAddSubgroup H).relIndex (toAddSubgroup K) = H.relIndex K

@[deprecated Subgroup.relIndex_toAddSubgroup (since := "2025-08-12")]

theorem Subgroup.relindex_toAddSubgroup {G : Type u_1} [Group G] {H K : Subgroup G} : (toAddSubgroup H).relIndex (toAddSubgroup K) = H.relIndex K

Alias of Subgroup.relIndex_toAddSubgroup.

@[simp]

theorem AddSubgroup.relIndex_toSubgroup {G : Type u_3} [AddGroup G] (H K : AddSubgroup G) : (toSubgroup H).relIndex (toSubgroup K) = H.relIndex K

@[deprecated AddSubgroup.relIndex_toSubgroup (since := "2025-08-12")]

theorem AddSubgroup.relindex_toSubgroup {G : Type u_3} [AddGroup G] (H K : AddSubgroup G) : (toSubgroup H).relIndex (toSubgroup K) = H.relIndex K

Alias of AddSubgroup.relIndex_toSubgroup.

class AddSubgroup.FiniteIndex {G : Type u_3} [AddGroup G] (H : AddSubgroup G) : Prop

Typeclass for finite index subgroups.

• index_ne_zero : H.index ≠ 0

  The additive subgroup has finite index; recall that AddSubgroup.index returns 0 when the index is infinite.

class Subgroup.FiniteIndex {G : Type u_1} [Group G] (H : Subgroup G) : Prop

Typeclass for finite index subgroups.

• index_ne_zero : H.index ≠ 0

  The subgroup has finite index; recall that Subgroup.index returns 0 when the index is infinite.

@[deprecated Subgroup.FiniteIndex.index_ne_zero (since := "2025-04-13")]

theorem Subgroup.FiniteIndex.finiteIndex {G : Type u_1} {inst✝ : Group G} {H : Subgroup G} [self : H.FiniteIndex] : H.index ≠ 0

Alias of Subgroup.FiniteIndex.index_ne_zero.

---

The subgroup has finite index; recall that Subgroup.index returns 0 when the index is infinite.

class AddSubgroup.IsFiniteRelIndex {G : Type u_3} [AddGroup G] (H K : AddSubgroup G) : Prop

Typeclass for a subgroup H to have finite index in a subgroup K.

• relIndex_ne_zero : H.relIndex K ≠ 0

class Subgroup.IsFiniteRelIndex {G : Type u_1} [Group G] (H K : Subgroup G) : Prop

Typeclass for a subgroup H to have finite index in a subgroup K.

• relIndex_ne_zero : H.relIndex K ≠ 0

theorem Subgroup.relIndex_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K] : H.relIndex K ≠ 0

theorem AddSubgroup.relIndex_ne_zero {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.IsFiniteRelIndex K] : H.relIndex K ≠ 0

@[deprecated Subgroup.relIndex_ne_zero (since := "2025-08-12")]

theorem Subgroup.relindex_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K] : H.relIndex K ≠ 0

Alias of Subgroup.relIndex_ne_zero.

instance Subgroup.IsFiniteRelIndex.to_finiteIndex_subgroupOf {G : Type u_1} [Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K] : (H.subgroupOf K).FiniteIndex

instance AddSubgroup.IsFiniteRelIndex.to_finiteIndex_addSubgroupOf {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.IsFiniteRelIndex K] : (H.addSubgroupOf K).FiniteIndex

theorem Subgroup.finiteIndex_iff {G : Type u_1} [Group G] {H : Subgroup G} : H.FiniteIndex ↔ H.index ≠ 0

theorem AddSubgroup.finiteIndex_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.FiniteIndex ↔ H.index ≠ 0

theorem Subgroup.not_finiteIndex_iff {G : Type u_3} [Group G] {H : Subgroup G} : ¬H.FiniteIndex ↔ H.index = 0

theorem AddSubgroup.not_finiteIndex_iff {G : Type u_3} [AddGroup G] {H : AddSubgroup G} : ¬H.FiniteIndex ↔ H.index = 0

noncomputable def Subgroup.fintypeQuotientOfFiniteIndex {G : Type u_1} [Group G] {H : Subgroup G} [H.FiniteIndex] : Fintype (G ⧸ H)

A finite index subgroup has finite quotient.

Equations

• Subgroup.fintypeQuotientOfFiniteIndex = Subgroup.fintypeOfIndexNeZero ⋯

noncomputable def AddSubgroup.fintypeQuotientOfFiniteIndex {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [H.FiniteIndex] : Fintype (G ⧸ H)

A finite index subgroup has finite quotient

Equations

• AddSubgroup.fintypeQuotientOfFiniteIndex = AddSubgroup.fintypeOfIndexNeZero ⋯

instance Subgroup.finite_quotient_of_finiteIndex {G : Type u_1} [Group G] {H : Subgroup G} [H.FiniteIndex] : Finite (G ⧸ H)

instance AddSubgroup.finite_quotient_of_finiteIndex {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [H.FiniteIndex] : Finite (G ⧸ H)

theorem Subgroup.finiteIndex_of_finite_quotient {G : Type u_1} [Group G] {H : Subgroup G} [Finite (G ⧸ H)] : H.FiniteIndex

theorem AddSubgroup.finiteIndex_of_finite_quotient {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [Finite (G ⧸ H)] : H.FiniteIndex

theorem Subgroup.finiteIndex_iff_finite_quotient {G : Type u_1} [Group G] {H : Subgroup G} : H.FiniteIndex ↔ Finite (G ⧸ H)

theorem AddSubgroup.finiteIndex_iff_finite_quotient {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.FiniteIndex ↔ Finite (G ⧸ H)

@[instance 100]

instance Subgroup.finiteIndex_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] : H.FiniteIndex

@[instance 100]

instance AddSubgroup.finiteIndex_of_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [Finite G] : H.FiniteIndex

theorem Subgroup.finite_iff_finite_and_finiteIndex {G : Type u_1} [Group G] (H : Subgroup G) : Finite G ↔ Finite ↥H ∧ H.FiniteIndex

theorem AddSubgroup.finite_iff_finite_and_finiteIndex {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Finite G ↔ Finite ↥H ∧ H.FiniteIndex

theorem MonoidHom.finite_iff_finite_ker_range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range

theorem AddMonoidHom.finite_iff_finite_ker_range {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') : Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range

instance Subgroup.instFiniteIndexTop {G : Type u_1} [Group G] : ⊤.FiniteIndex

instance AddSubgroup.instFiniteIndexTop {G : Type u_1} [AddGroup G] : ⊤.FiniteIndex

instance Subgroup.instFiniteIndexMin {G : Type u_1} [Group G] {H K : Subgroup G} [H.FiniteIndex] [K.FiniteIndex] : (H ⊓ K).FiniteIndex

instance AddSubgroup.instFiniteIndexMin {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex] [K.FiniteIndex] : (H ⊓ K).FiniteIndex

theorem Subgroup.finiteIndex_iInf {G : Type u_1} [Group G] {ι : Type u_3} [Finite ι] {f : ι → Subgroup G} (hf : ∀ (i : ι), (f i).FiniteIndex) : (⨅ (i : ι), f i).FiniteIndex

theorem AddSubgroup.finiteIndex_iInf {G : Type u_1} [AddGroup G] {ι : Type u_3} [Finite ι] {f : ι → AddSubgroup G} (hf : ∀ (i : ι), (f i).FiniteIndex) : (⨅ (i : ι), f i).FiniteIndex

theorem Subgroup.finiteIndex_iInf' {G : Type u_1} [Group G] {ι : Type u_3} {s : Finset ι} (f : ι → Subgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) : (⨅ i ∈ s, f i).FiniteIndex

theorem AddSubgroup.finiteIndex_iInf' {G : Type u_1} [AddGroup G] {ι : Type u_3} {s : Finset ι} (f : ι → AddSubgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) : (⨅ i ∈ s, f i).FiniteIndex

instance Subgroup.instFiniteIndex_subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) [H.FiniteIndex] : (H.subgroupOf K).FiniteIndex

instance AddSubgroup.instFiniteIndex_addSubgroupOf {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [H.FiniteIndex] : (H.addSubgroupOf K).FiniteIndex

theorem Subgroup.finiteIndex_of_le {G : Type u_1} [Group G] {H K : Subgroup G} [H.FiniteIndex] (h : H ≤ K) : K.FiniteIndex

theorem AddSubgroup.finiteIndex_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex] (h : H ≤ K) : K.FiniteIndex

theorem Subgroup.index_antitone {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) [H.FiniteIndex] : K.index ≤ H.index

theorem AddSubgroup.index_antitone {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) [H.FiniteIndex] : K.index ≤ H.index

theorem Subgroup.index_strictAnti {G : Type u_1} [Group G] {H K : Subgroup G} (h : H < K) [H.FiniteIndex] : K.index < H.index

theorem AddSubgroup.index_strictAnti {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H < K) [H.FiniteIndex] : K.index < H.index

instance Subgroup.finiteIndex_ker {G : Type u_1} [Group G] {G' : Type u_3} [Group G'] (f : G →* G') [Finite ↥f.range] : f.ker.FiniteIndex

instance AddSubgroup.finiteIndex_ker {G : Type u_1} [AddGroup G] {G' : Type u_3} [AddGroup G'] (f : G →+ G') [Finite ↥f.range] : f.ker.FiniteIndex

instance Subgroup.finiteIndex_normalCore {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] : H.normalCore.FiniteIndex

theorem Subgroup.index_range {G : Type u_1} [Group G] {f : G →* G} [hf : f.ker.FiniteIndex] : f.range.index = Nat.card ↥f.ker

theorem AddSubgroup.index_range {G : Type u_1} [AddGroup G] {f : G →+ G} [hf : f.ker.FiniteIndex] : f.range.index = Nat.card ↥f.ker

theorem Subgroup.relIndex_pointwise_smul {G : Type u_1} {H : Type u_2} [Group H] (h : H) [Group G] [MulDistribMulAction H G] (J K : Subgroup G) : (h • J).relIndex (h • K) = J.relIndex K

@[deprecated Subgroup.relIndex_pointwise_smul (since := "2025-08-12")]

theorem Subgroup.relindex_pointwise_smul {G : Type u_1} {H : Type u_2} [Group H] (h : H) [Group G] [MulDistribMulAction H G] (J K : Subgroup G) : (h • J).relIndex (h • K) = J.relIndex K

Alias of Subgroup.relIndex_pointwise_smul.

theorem AddSubgroup.relIndex_pointwise_smul {G : Type u_1} {H : Type u_2} [Group H] (h : H) [AddGroup G] [DistribMulAction H G] (J K : AddSubgroup G) : (h • J).relIndex (h • K) = J.relIndex K

@[deprecated AddSubgroup.relIndex_pointwise_smul (since := "2025-08-12")]

theorem AddSubgroup.relindex_pointwise_smul {G : Type u_1} {H : Type u_2} [Group H] (h : H) [AddGroup G] [DistribMulAction H G] (J K : AddSubgroup G) : (h • J).relIndex (h • K) = J.relIndex K

Alias of AddSubgroup.relIndex_pointwise_smul.

theorem MulAction.index_stabilizer (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (x : X) : (stabilizer G x).index = (orbit G x).ncard

theorem AddAction.index_stabilizer (G : Type u_1) {X : Type u_2} [AddGroup G] [AddAction G X] (x : X) : (stabilizer G x).index = (orbit G x).ncard

theorem MulAction.index_stabilizer_of_transitive (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (x : X) [IsPretransitive G X] : (stabilizer G x).index = Nat.card X

theorem AddAction.index_stabilizer_of_transitive (G : Type u_1) {X : Type u_2} [AddGroup G] [AddAction G X] (x : X) [IsPretransitive G X] : (stabilizer G x).index = Nat.card X

theorem MonoidHom.surjective_of_card_ker_le_div {G : Type u_1} {M : Type u_2} [Group G] [Group M] [Finite G] [Finite M] (f : G →* M) (h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M) : Function.Surjective ⇑f

theorem AddMonoidHom.surjective_of_card_ker_le_div {G : Type u_1} {M : Type u_2} [AddGroup G] [AddGroup M] [Finite G] [Finite M] (f : G →+ M) (h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M) : Function.Surjective ⇑f

theorem MonoidHom.card_fiber_eq_of_mem_range {G : Type u_1} {M : Type u_2} {F : Type u_3} [Group G] [Fintype G] [Monoid M] [DecidableEq M] [FunLike F G M] [MonoidHomClass F G M] (f : F) {x y : M} (hx : x ∈ Set.range ⇑f) (hy : y ∈ Set.range ⇑f) : {g : G | f g = x}.card = {g : G | f g = y}.card

theorem AddMonoidHom.card_fiber_eq_of_mem_range {G : Type u_1} {M : Type u_2} {F : Type u_3} [AddGroup G] [Fintype G] [AddMonoid M] [DecidableEq M] [FunLike F G M] [AddMonoidHomClass F G M] (f : F) {x y : M} (hx : x ∈ Set.range ⇑f) (hy : y ∈ Set.range ⇑f) : {g : G | f g = x}.card = {g : G | f g = y}.card

@[simp]

theorem AddSubgroup.index_smul {G : Type u_1} {A : Type u_2} [Group G] [AddGroup A] [DistribMulAction G A] (a : G) (S : AddSubgroup A) : (a • S).index = S.index