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
      • H.relindex K = (H.subgroupOf K).index
      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
        • H.relindex K = (H.addSubgroupOf K).index
        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) :
          (Subgroup.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) :
          (AddSubgroup.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) :
          (Subgroup.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) :
          (AddSubgroup.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') :
          (Subgroup.comap f H).relindex K = H.relindex (Subgroup.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') :
          (AddSubgroup.comap f H).relindex K = H.relindex (AddSubgroup.map f K)
          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
          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
          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
          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
          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
          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
          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
          @[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
          @[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
          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
          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
          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
          @[deprecated Subgroup.index_bot]
          theorem Subgroup.index_bot_eq_card {G : Type u_1} [Group G] :
          .index = Nat.card G

          Alias of Subgroup.index_bot.

          @[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
          @[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
          @[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]
          theorem Subgroup.relindex_bot_left_eq_card {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
          @[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') :
          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 (Subgroup.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 (AddSubgroup.map f K)
          @[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
          @[deprecated Subgroup.card_dvd_of_injective]
          theorem Subgroup.nat_card_dvd_of_injective {α : Type u_1} [Group α] {H : Type u_2} [Group H] (f : α →* H) (hf : Function.Injective f) :

          Alias of Subgroup.card_dvd_of_injective.

          @[deprecated Subgroup.card_dvd_of_le]
          theorem Subgroup.nat_card_dvd_of_le {α : Type u_1} [Group α] {H K : Subgroup α} (hHK : H K) :

          Alias of Subgroup.card_dvd_of_le.

          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) :
          @[deprecated Subgroup.card_dvd_of_surjective]
          theorem Subgroup.nat_card_dvd_of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (hf : Function.Surjective f) :

          Alias of Subgroup.card_dvd_of_surjective.

          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') :
          theorem AddSubgroup.card_map_dvd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') :
          theorem Subgroup.index_map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') :
          (Subgroup.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') :
          (AddSubgroup.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) :
          (Subgroup.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) :
          (AddSubgroup.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 (Subgroup.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 (AddSubgroup.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) :
          (Subgroup.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) :
          (AddSubgroup.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) :
          (Subgroup.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) :
          (AddSubgroup.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) :
          (Subgroup.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) :
          (AddSubgroup.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 G
          theorem AddSubgroup.relindex_dvd_card {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
          H.relindex K Nat.card 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.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
          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
          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
          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
          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
          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_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
          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
          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)) :
          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 =
          @[deprecated AddSubgroup.inf_eq_bot_of_coprime]
          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)) :
          H K =

          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)] :
          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
          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.index_eq_zero_iff_infinite {G : Type u_1} [Group G] {H : Subgroup G} :
              H.index = 0 Infinite (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.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
              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 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 < mm H.relindex Km n) :
              n a H K
              @[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_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
              @[simp]
              theorem Subgroup.index_pi {G : Type u_1} [Group G] {ι : Type u_3} [Fintype ι] (H : ιSubgroup G) :
              (Subgroup.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) :
              (AddSubgroup.pi Set.univ H).index = i : ι, (H i).index
              @[simp]
              theorem Subgroup.index_toAddSubgroup {G : Type u_1} [Group G] {H : Subgroup G} :
              (Subgroup.toAddSubgroup H).index = H.index
              @[simp]
              theorem AddSubgroup.index_toSubgroup {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :
              (AddSubgroup.toSubgroup H).index = H.index
              @[simp]
              theorem Subgroup.relindex_toAddSubgroup {G : Type u_1} [Group G] {H K : Subgroup G} :
              (Subgroup.toAddSubgroup H).relindex (Subgroup.toAddSubgroup K) = H.relindex K
              @[simp]
              theorem AddSubgroup.relindex_toSubgroup {G : Type u_3} [AddGroup G] (H K : AddSubgroup G) :
              (AddSubgroup.toSubgroup H).relindex (AddSubgroup.toSubgroup K) = H.relindex K
              class Subgroup.FiniteIndex {G : Type u_1} [Group G] (H : Subgroup G) :

              Typeclass for finite index subgroups.

              • finiteIndex : H.index 0

                The subgroup has finite index

              Instances

                Typeclass for finite index subgroups.

                • finiteIndex : H.index 0

                  The additive subgroup has finite index

                Instances
                  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 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
                      @[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
                      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 : 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
                      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
                      instance Subgroup.finiteIndex_center (G : Type u_1) [Group G] [Finite (commutatorSet G)] [Group.FG G] :
                      (Subgroup.center G).FiniteIndex
                      theorem MulAction.index_stabilizer (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (x : X) :
                      (MulAction.stabilizer G x).index = (MulAction.orbit G x).ncard
                      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) :
                      (Finset.filter (fun (g : G) => f g = x) Finset.univ).card = (Finset.filter (fun (g : G) => f g = y) Finset.univ).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) :
                      (Finset.filter (fun (g : G) => f g = x) Finset.univ).card = (Finset.filter (fun (g : G) => f g = y) Finset.univ).card