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
                  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)
                  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) :
                  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) :
                  theorem Subgroup.relindex_subgroupOf {G : Type u_1} [Group G] {H K L : Subgroup G} (hKL : K L) :
                  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) :
                  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
                  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
                  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
                  @[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
                  @[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
                  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) :
                  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]
                  @[simp]
                  theorem Subgroup.relindex_top_right {G : Type u_1} [Group G] (H : Subgroup G) :
                  @[simp]
                  theorem Subgroup.relindex_bot_left {G : Type u_1} [Group G] (H : Subgroup G) :
                  @[simp]
                  @[simp]
                  theorem Subgroup.relindex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) :
                  @[simp]
                  @[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
                  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)
                  @[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
                  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) :
                  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
                  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
                  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.

                  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 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) :
                  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) :
                  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) :
                  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
                  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.

                  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
                  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
                  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
                  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
                  @[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 =
                  @[deprecated AddSubgroup.inf_eq_bot_of_coprime (since := "2024-12-18")]
                  theorem add_inf_eq_bot_of_coprime {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : (Nat.card H).Coprime (Nat.card K)) :
                  HK =

                  Alias of AddSubgroup.inf_eq_bot_of_coprime.

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

                          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] :
                                  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]
                                          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
                                          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
                                          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