Documentation

Mathlib.GroupTheory.Index

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 #

Main results #

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
Instances For
    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
    Instances For
      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
      Instances For
        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
        Instances For
          @[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
          Instances For
            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) :
            theorem AddSubgroup.index_comap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G' →+ G) :
            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) = (Hf.ker).relIndex (Kf.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) = (Hf.ker).relIndex (Kf.ker)
            theorem Subgroup.relIndex_mul_index {G : Type u_1} [Group G] {H K : Subgroup G} (h : H K) :
            theorem AddSubgroup.relIndex_mul_index {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H K) :
            @[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) :

            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) :
            theorem AddSubgroup.index_dvd_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H K) :
            theorem Subgroup.relIndex_dvd_index_of_le {G : Type u_1} [Group G] {H K : Subgroup G} (h : H K) :
            theorem AddSubgroup.relIndex_dvd_index_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H K) :
            @[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) :

            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) :
            @[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) :

            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) :
            theorem AddSubgroup.relIndex_mul_relIndex {G : Type u_1} [AddGroup G] (H K L : AddSubgroup G) (hHK : H K) (hKL : K 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) :

            Alias of Subgroup.relIndex_mul_relIndex.

            theorem Subgroup.inf_relIndex_right {G : Type u_1} [Group G] (H K : Subgroup G) :
            (HK).relIndex K = H.relIndex K
            theorem AddSubgroup.inf_relIndex_right {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
            (HK).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) :
            (HK).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) :
            (HK).relIndex H = K.relIndex H
            theorem AddSubgroup.inf_relIndex_left {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
            (HK).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) :
            (HK).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 (KL) * K.relIndex L = (HK).relIndex L
            theorem AddSubgroup.relIndex_inf_mul_relIndex {G : Type u_1} [AddGroup G] (H K L : AddSubgroup G) :
            H.relIndex (KL) * K.relIndex L = (HK).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 (KL) * K.relIndex L = (HK).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 (HK) = K.relIndex H
            @[simp]
            theorem AddSubgroup.relIndex_sup_right {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.Normal] :
            K.relIndex (HK) = 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 (HK) = 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 (KH) = K.relIndex H
            @[simp]
            theorem AddSubgroup.relIndex_sup_left {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.Normal] :
            K.relIndex (KH) = 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 (KH) = K.relIndex H

            Alias of Subgroup.relIndex_sup_left.

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

            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) :
            theorem AddSubgroup.relIndex_dvd_of_le_left {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (L : AddSubgroup G) (hHK : H K) :
            @[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) :

            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] :
            @[simp]
            theorem AddSubgroup.index_top {G : Type u_1} [AddGroup G] :
            @[simp]
            theorem Subgroup.index_bot {G : Type u_1} [Group G] :
            @[simp]
            @[simp]
            theorem Subgroup.relIndex_top_left {G : Type u_1} [Group G] (H : Subgroup G) :
            @[simp]
            @[deprecated Subgroup.relIndex_top_left (since := "2025-08-12")]
            theorem Subgroup.relindex_top_left {G : Type u_1} [Group G] (H : Subgroup G) :

            Alias of Subgroup.relIndex_top_left.

            @[simp]
            theorem Subgroup.relIndex_top_right {G : Type u_1} [Group G] (H : Subgroup G) :
            @[deprecated Subgroup.relIndex_top_right (since := "2025-08-12")]
            theorem Subgroup.relindex_top_right {G : Type u_1} [Group G] (H : Subgroup G) :

            Alias of Subgroup.relIndex_top_right.

            @[simp]
            theorem Subgroup.relIndex_bot_left {G : Type u_1} [Group G] (H : Subgroup G) :
            @[simp]
            @[deprecated Subgroup.relIndex_bot_left (since := "2025-08-12")]
            theorem Subgroup.relindex_bot_left {G : Type u_1} [Group G] (H : Subgroup G) :

            Alias of Subgroup.relIndex_bot_left.

            @[simp]
            theorem Subgroup.relIndex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) :
            @[simp]
            @[deprecated Subgroup.relIndex_bot_right (since := "2025-08-12")]
            theorem Subgroup.relindex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) :

            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') :
            theorem AddSubgroup.index_ker {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') :
            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) :
            @[simp]
            theorem AddSubgroup.card_mul_index {G : Type u_1} [AddGroup G] (H : AddSubgroup 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) :
            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) :
            theorem Subgroup.card_range_dvd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') :
            theorem AddSubgroup.card_range_dvd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ 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 = (Hf.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 = (Hf.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) :
            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) :
            theorem Subgroup.index_map_subtype {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup H) :
            theorem Subgroup.index_eq_card {G : Type u_1} [Group G] (H : Subgroup G) :
            theorem Subgroup.index_mul_card {G : Type u_1} [Group G] (H : Subgroup G) :
            theorem Subgroup.relIndex_dvd_card {G : Type u_1} [Group G] (H K : Subgroup G) :
            @[deprecated Subgroup.relIndex_dvd_card (since := "2025-08-12")]
            theorem Subgroup.relindex_dvd_card {G : Type u_1} [Group G] (H K : Subgroup G) :

            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
            @[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) :
            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) :
            @[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) :

            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) :
            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) :
            @[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) :

            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) :
            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) :
            @[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) :

            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) :
            (HK).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) :
            (HK).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) :
            (HK).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) :
            (HK).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) :
            (HK).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) :
            (JL).relIndex (KL) 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) :
            (JL).relIndex (KL) 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) :
            (JL).relIndex (KL) 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} :
            (HK).relIndex L H.relIndex L * K.relIndex L
            theorem AddSubgroup.relIndex_inf_le {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} :
            (HK).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} :
            (HK).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} :
            (HK).index H.index * K.index
            theorem AddSubgroup.index_inf_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} :
            (HK).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)) :
            HK =
            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)) :
            HK =
            theorem Subgroup.index_ne_zero_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [hH : Finite (G H)] :
            theorem AddSubgroup.index_ne_zero_of_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : Finite (G H)] :
            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
            Instances For
              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
              Instances For
                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.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 HK
                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 HK
                @[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 HK

                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 < mm H.indexm 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 < mm H.indexm 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 < mm H.relIndex Km n) :
                a ^ n HK
                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 < mm H.relIndex Km n) :
                n a HK
                @[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 < mm H.relIndex Km n) :
                a ^ n HK

                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]
                @[simp]
                @[deprecated Subgroup.relIndex_toAddSubgroup (since := "2025-08-12")]

                Alias of Subgroup.relIndex_toAddSubgroup.

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

                Alias of AddSubgroup.relIndex_toSubgroup.

                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.

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

                  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.

                  Instances
                    @[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] :

                    Alias of Subgroup.FiniteIndex.index_ne_zero.


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

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

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

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

                      Instances
                        theorem Subgroup.relIndex_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K] :
                        @[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] :

                        Alias of Subgroup.relIndex_ne_zero.

                        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
                        Instances For
                          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
                          Instances For
                            @[instance 100]
                            instance Subgroup.finiteIndex_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] :
                            @[instance 100]
                            theorem MonoidHom.finite_iff_finite_ker_range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') :
                            theorem AddMonoidHom.finite_iff_finite_ker_range {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') :
                            instance Subgroup.instFiniteIndexMin {G : Type u_1} [Group G] {H K : Subgroup G} [H.FiniteIndex] [K.FiniteIndex] :
                            (HK).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 : is, (f i).FiniteIndex) :
                            (⨅ is, f i).FiniteIndex
                            theorem AddSubgroup.finiteIndex_iInf' {G : Type u_1} [AddGroup G] {ι : Type u_3} {s : Finset ι} (f : ιAddSubgroup G) (hs : is, (f i).FiniteIndex) :
                            (⨅ is, f i).FiniteIndex
                            theorem Subgroup.finiteIndex_of_le {G : Type u_1} [Group G] {H K : Subgroup G} [H.FiniteIndex] (h : H K) :
                            theorem Subgroup.index_antitone {G : Type u_1} [Group G] {H K : Subgroup G} (h : H K) [H.FiniteIndex] :
                            theorem AddSubgroup.index_antitone {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H K) [H.FiniteIndex] :
                            theorem Subgroup.index_strictAnti {G : Type u_1} [Group G] {H K : Subgroup G} (h : H < K) [H.FiniteIndex] :
                            theorem AddSubgroup.index_strictAnti {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H < K) [H.FiniteIndex] :
                            instance Subgroup.finiteIndex_ker {G : Type u_1} [Group G] {G' : Type u_3} [Group G'] (f : G →* G') [Finite f.range] :
                            instance AddSubgroup.finiteIndex_ker {G : Type u_1} [AddGroup G] {G' : Type u_3} [AddGroup G'] (f : G →+ G') [Finite f.range] :
                            theorem Subgroup.index_range {G : Type u_1} [Group G] {f : G →* G} [hf : f.ker.FiniteIndex] :
                            theorem AddSubgroup.index_range {G : Type u_1} [AddGroup G] {f : G →+ G} [hf : f.ker.FiniteIndex] :
                            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) :
                            theorem AddAction.index_stabilizer (G : Type u_1) {X : Type u_2} [AddGroup G] [AddAction G X] (x : 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) :
                            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