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 #

source
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
    source
    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
      source
      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
        source
        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
          source
          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
          source
          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
          source
          theorem Subgroup.index_comap {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G' →* G) :
          (comap f H).index = H.relindex f.range
          source
          theorem AddSubgroup.index_comap {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G' →+ G) :
          (comap f H).index = H.relindex f.range
          source
          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)
          source
          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)
          source
          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
          source
          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
          source
          theorem Subgroup.index_dvd_of_le {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) :
          K.index ∣ H.index
          source
          theorem AddSubgroup.index_dvd_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) :
          K.index ∣ H.index
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          theorem Subgroup.inf_relindex_right {G : Type u_1} [Group G] (H K : Subgroup G) :
          (H ⊓ K).relindex K = H.relindex K
          source
          theorem AddSubgroup.inf_relindex_right {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
          (H ⊓ K).relindex K = H.relindex K
          source
          theorem Subgroup.inf_relindex_left {G : Type u_1} [Group G] (H K : Subgroup G) :
          (H ⊓ K).relindex H = K.relindex H
          source
          theorem AddSubgroup.inf_relindex_left {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
          (H ⊓ K).relindex H = K.relindex H
          source
          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
          source
          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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          theorem Subgroup.relindex_dvd_index_of_normal {G : Type u_1} [Group G] (H K : Subgroup G) [H.Normal] :
          H.relindex K ∣ H.index
          source
          theorem AddSubgroup.relindex_dvd_index_of_normal {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [H.Normal] :
          H.relindex K ∣ H.index
          source
          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
          source
          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
          source
          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.

          source
          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.

          source
          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)
          source
          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)
          source
          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
          source
          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
          source
          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
          source
          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
          source
          @[simp]
          theorem Subgroup.index_top {G : Type u_1} [Group G] :
          ⊤.index = 1
          source
          @[simp]
          theorem AddSubgroup.index_top {G : Type u_1} [AddGroup G] :
          ⊤.index = 1
          source
          @[simp]
          theorem Subgroup.index_bot {G : Type u_1} [Group G] :
          ⊥.index = Nat.card G
          source
          @[simp]
          theorem AddSubgroup.index_bot {G : Type u_1} [AddGroup G] :
          ⊥.index = Nat.card G
          source
          @[simp]
          theorem Subgroup.relindex_top_left {G : Type u_1} [Group G] (H : Subgroup G) :
          ⊤.relindex H = 1
          source
          @[simp]
          theorem AddSubgroup.relindex_top_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          ⊤.relindex H = 1
          source
          @[simp]
          theorem Subgroup.relindex_top_right {G : Type u_1} [Group G] (H : Subgroup G) :
          H.relindex ⊤ = H.index
          source
          @[simp]
          theorem AddSubgroup.relindex_top_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          H.relindex ⊤ = H.index
          source
          @[simp]
          theorem Subgroup.relindex_bot_left {G : Type u_1} [Group G] (H : Subgroup G) :
          ⊥.relindex H = Nat.card ↥H
          source
          @[simp]
          theorem AddSubgroup.relindex_bot_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          ⊥.relindex H = Nat.card ↥H
          source
          @[simp]
          theorem Subgroup.relindex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) :
          H.relindex ⊥ = 1
          source
          @[simp]
          theorem AddSubgroup.relindex_bot_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          H.relindex ⊥ = 1
          source
          @[simp]
          theorem Subgroup.relindex_self {G : Type u_1} [Group G] (H : Subgroup G) :
          H.relindex H = 1
          source
          @[simp]
          theorem AddSubgroup.relindex_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          H.relindex H = 1
          source
          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
          source
          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
          source
          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)
          source
          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)
          source
          @[simp]
          theorem Subgroup.card_mul_index {G : Type u_1} [Group G] (H : Subgroup G) :
          Nat.card ↥H * H.index = Nat.card G
          source
          @[simp]
          theorem AddSubgroup.card_mul_index {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          Nat.card ↥H * H.index = Nat.card G
          source
          theorem Subgroup.card_dvd_of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (hf : Function.Surjective ⇑f) :
          Nat.card G' ∣ Nat.card G
          source
          theorem AddSubgroup.card_dvd_of_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (hf : Function.Surjective ⇑f) :
          Nat.card G' ∣ Nat.card G
          source
          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
          source
          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
          source
          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
          source
          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
          source
          theorem Subgroup.index_map {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') :
          (map f H).index = (H ⊔ f.ker).index * f.range.index
          source
          theorem AddSubgroup.index_map {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') :
          (map f H).index = (H ⊔ f.ker).index * f.range.index
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          @[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
          source
          @[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
          source
          theorem Subgroup.index_map_of_injective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {f : G →* G'} (hf : Function.Injective ⇑f) :
          (map f H).index = H.index * f.range.index
          source
          theorem AddSubgroup.index_map_of_injective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : Function.Injective ⇑f) :
          (map f H).index = H.index * f.range.index
          source
          theorem Subgroup.index_map_subtype {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) :
          (map H.subtype K).index = K.index * H.index
          source
          theorem AddSubgroup.index_map_subtype {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) :
          (map H.subtype K).index = K.index * H.index
          source
          theorem Subgroup.index_eq_card {G : Type u_1} [Group G] (H : Subgroup G) :
          H.index = Nat.card (G ⧸ H)
          source
          theorem AddSubgroup.index_eq_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          H.index = Nat.card (G ⧸ H)
          source
          theorem Subgroup.index_mul_card {G : Type u_1} [Group G] (H : Subgroup G) :
          H.index * Nat.card ↥H = Nat.card G
          source
          theorem AddSubgroup.index_mul_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          H.index * Nat.card ↥H = Nat.card G
          source
          theorem Subgroup.index_dvd_card {G : Type u_1} [Group G] (H : Subgroup G) :
          H.index ∣ Nat.card G
          source
          theorem AddSubgroup.index_dvd_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
          H.index ∣ Nat.card G
          source
          theorem Subgroup.relindex_dvd_card {G : Type u_1} [Group G] (H K : Subgroup G) :
          H.relindex K ∣ Nat.card ↥K
          source
          theorem AddSubgroup.relindex_dvd_card {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) :
          H.relindex K ∣ Nat.card ↥K
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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.

          source
          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.

          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          theorem Subgroup.relindex_inter_ne_zero {G : Type u_1} [Group G] {J K : Subgroup G} (hJK : J.relindex K ≠ 0) (L : Subgroup G) :
          (J ⊓ L).relindex (K ⊓ L) ≠ 0

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

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

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

          source
          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
          source
          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
          source
          theorem Subgroup.index_inf_le {G : Type u_1} [Group G] {H K : Subgroup G} :
          (H ⊓ K).index ≤ H.index * K.index
          source
          theorem AddSubgroup.index_inf_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} :
          (H ⊓ K).index ≤ H.index * K.index
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          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
          source
          @[simp]
          theorem Subgroup.index_eq_one {G : Type u_1} [Group G] {H : Subgroup G} :
          H.index = 1 ↔ H = ⊤
          source
          @[simp]
          theorem AddSubgroup.index_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
          H.index = 1 ↔ H = ⊤
          source
          @[simp]
          theorem Subgroup.relindex_eq_one {G : Type u_1} [Group G] {H K : Subgroup G} :
          H.relindex K = 1 ↔ K ≤ H
          source
          @[simp]
          theorem AddSubgroup.relindex_eq_one {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} :
          H.relindex K = 1 ↔ K ≤ H
          source
          @[simp]
          theorem Subgroup.card_eq_one {G : Type u_1} [Group G] {H : Subgroup G} :
          Nat.card ↥H = 1 ↔ H = ⊥
          source
          @[simp]
          theorem AddSubgroup.card_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
          Nat.card ↥H = 1 ↔ H = ⊥
          source
          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 = ⊥
          source
          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 = ⊥
          source
          @[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)) :
          H ⊓ K = ⊥

          Alias of AddSubgroup.inf_eq_bot_of_coprime.

          source
          theorem Subgroup.index_ne_zero_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [hH : Finite (G ⧸ H)] :
          H.index ≠ 0
          source
          theorem AddSubgroup.index_ne_zero_of_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : Finite (G ⧸ H)] :
          H.index ≠ 0
          source
          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
            source
            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
              source
              theorem Subgroup.index_eq_zero_iff_infinite {G : Type u_1} [Group G] {H : Subgroup G} :
              H.index = 0 ↔ Infinite (G ⧸ H)
              source
              theorem AddSubgroup.index_eq_zero_iff_infinite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
              H.index = 0 ↔ Infinite (G ⧸ H)
              source
              theorem Subgroup.index_ne_zero_iff_finite {G : Type u_1} [Group G] {H : Subgroup G} :
              H.index ≠ 0 ↔ Finite (G ⧸ H)
              source
              theorem AddSubgroup.index_ne_zero_iff_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
              H.index ≠ 0 ↔ Finite (G ⧸ H)
              source
              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
              source
              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
              source
              theorem Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {X : Type u_3} [MulAction G X] [Finite (MulAction.orbitRel.Quotient G X)] (hi : H.index ≠ 0) :
              Finite (MulAction.orbitRel.Quotient (↥H) X)
              source
              theorem AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {X : Type u_3} [AddAction G X] [Finite (AddAction.orbitRel.Quotient G X)] (hi : H.index ≠ 0) :
              Finite (AddAction.orbitRel.Quotient (↥H) X)
              source
              theorem Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {X : Type u_3} [MulAction G X] [MulAction.IsPretransitive G X] (hi : H.index ≠ 0) :
              Finite (MulAction.orbitRel.Quotient (↥H) X)
              source
              theorem AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {X : Type u_3} [AddAction G X] [AddAction.IsPretransitive G X] (hi : H.index ≠ 0) :
              Finite (AddAction.orbitRel.Quotient (↥H) X)
              source
              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
              source
              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
              source
              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
              source
              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
              source
              theorem Subgroup.pow_mem_of_index_ne_zero_of_dvd {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index ≠ 0) (a : G) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n) :
              a ^ n ∈ H
              source
              theorem AddSubgroup.nsmul_mem_of_index_ne_zero_of_dvd {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index ≠ 0) (a : G) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n) :
              n • a ∈ H
              source
              theorem Subgroup.pow_mem_of_relindex_ne_zero_of_dvd {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.relindex K → m ∣ n) :
              a ^ n ∈ H ⊓ K
              source
              theorem AddSubgroup.nsmul_mem_of_relindex_ne_zero_of_dvd {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) {n : ℕ} (hn : ∀ (m : ℕ), 0 < m → m ≤ H.relindex K → m ∣ n) :
              n • a ∈ H ⊓ K
              source
              @[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
              source
              @[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
              source
              @[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.

              source
              @[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
              source
              @[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
              source
              @[simp]
              theorem Subgroup.index_toAddSubgroup {G : Type u_1} [Group G] {H : Subgroup G} :
              (toAddSubgroup H).index = H.index
              source
              @[simp]
              theorem AddSubgroup.index_toSubgroup {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :
              (toSubgroup H).index = H.index
              source
              @[simp]
              theorem Subgroup.relindex_toAddSubgroup {G : Type u_1} [Group G] {H K : Subgroup G} :
              (toAddSubgroup H).relindex (toAddSubgroup K) = H.relindex K
              source
              @[simp]
              theorem AddSubgroup.relindex_toSubgroup {G : Type u_3} [AddGroup G] (H K : AddSubgroup G) :
              (toSubgroup H).relindex (toSubgroup K) = H.relindex K
              source
              class AddSubgroup.FiniteIndex {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :
              Prop

              Typeclass for finite index subgroups.

              • index_ne_zero : H.index ≠ 0

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

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

                Typeclass for finite index subgroups.

                • index_ne_zero : H.index ≠ 0

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

                Instances
                  source
                  @[deprecated Subgroup.FiniteIndex.index_ne_zero (since := "2025-04-13")]
                  theorem Subgroup.FiniteIndex.finiteIndex {G : Type u_1} {inst✝ : Group G} {H : Subgroup G} [self : H.FiniteIndex] :
                  H.index ≠ 0

                  Alias of Subgroup.FiniteIndex.index_ne_zero.

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

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

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

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

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

                    Instances
                      source
                      theorem Subgroup.relindex_ne_zero {G : Type u_1} [Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K] :
                      H.relindex K ≠ 0
                      source
                      theorem AddSubgroup.relindex_ne_zero {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.IsFiniteRelIndex K] :
                      H.relindex K ≠ 0
                      source
                      instance Subgroup.IsFiniteRelIndex.to_finiteIndex_subgroupOf {G : Type u_1} [Group G] {H K : Subgroup G} [H.IsFiniteRelIndex K] :
                      (H.subgroupOf K).FiniteIndex
                      source
                      instance AddSubgroup.IsFiniteRelIndex.to_finiteIndex_addSubgroupOf {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.IsFiniteRelIndex K] :
                      (H.addSubgroupOf K).FiniteIndex
                      source
                      theorem Subgroup.finiteIndex_iff {G : Type u_1} [Group G] {H : Subgroup G} :
                      H.FiniteIndex ↔ H.index ≠ 0
                      source
                      theorem AddSubgroup.finiteIndex_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} :
                      H.FiniteIndex ↔ H.index ≠ 0
                      source
                      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
                        source
                        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
                          source
                          instance Subgroup.finite_quotient_of_finiteIndex {G : Type u_1} [Group G] {H : Subgroup G} [H.FiniteIndex] :
                          Finite (G ⧸ H)
                          source
                          instance AddSubgroup.finite_quotient_of_finiteIndex {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [H.FiniteIndex] :
                          Finite (G ⧸ H)
                          source
                          theorem Subgroup.finiteIndex_of_finite_quotient {G : Type u_1} [Group G] {H : Subgroup G} [Finite (G ⧸ H)] :
                          H.FiniteIndex
                          source
                          theorem AddSubgroup.finiteIndex_of_finite_quotient {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [Finite (G ⧸ H)] :
                          H.FiniteIndex
                          source
                          @[instance 100]
                          instance Subgroup.finiteIndex_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [Finite G] :
                          H.FiniteIndex
                          source
                          @[instance 100]
                          instance AddSubgroup.finiteIndex_of_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [Finite G] :
                          H.FiniteIndex
                          source
                          instance Subgroup.instFiniteIndexTop {G : Type u_1} [Group G] :
                          ⊤.FiniteIndex
                          source
                          instance AddSubgroup.instFiniteIndexTop {G : Type u_1} [AddGroup G] :
                          ⊤.FiniteIndex
                          source
                          instance Subgroup.instFiniteIndexMin {G : Type u_1} [Group G] {H K : Subgroup G} [H.FiniteIndex] [K.FiniteIndex] :
                          (H ⊓ K).FiniteIndex
                          source
                          instance AddSubgroup.instFiniteIndexMin {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex] [K.FiniteIndex] :
                          (H ⊓ K).FiniteIndex
                          source
                          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
                          source
                          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
                          source
                          theorem Subgroup.finiteIndex_iInf' {G : Type u_1} [Group G] {ι : Type u_3} {s : Finset ι} (f : ι → Subgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) :
                          (⨅ i ∈ s, f i).FiniteIndex
                          source
                          theorem AddSubgroup.finiteIndex_iInf' {G : Type u_1} [AddGroup G] {ι : Type u_3} {s : Finset ι} (f : ι → AddSubgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) :
                          (⨅ i ∈ s, f i).FiniteIndex
                          source
                          instance Subgroup.instFiniteIndex_subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) [H.FiniteIndex] :
                          (H.subgroupOf K).FiniteIndex
                          source
                          instance AddSubgroup.instFiniteIndex_addSubgroupOf {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [H.FiniteIndex] :
                          (H.addSubgroupOf K).FiniteIndex
                          source
                          theorem Subgroup.finiteIndex_of_le {G : Type u_1} [Group G] {H K : Subgroup G} [H.FiniteIndex] (h : H ≤ K) :
                          K.FiniteIndex
                          source
                          theorem AddSubgroup.finiteIndex_of_le {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex] (h : H ≤ K) :
                          K.FiniteIndex
                          source
                          theorem Subgroup.index_antitone {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) [H.FiniteIndex] :
                          K.index ≤ H.index
                          source
                          theorem AddSubgroup.index_antitone {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) [H.FiniteIndex] :
                          K.index ≤ H.index
                          source
                          theorem Subgroup.index_strictAnti {G : Type u_1} [Group G] {H K : Subgroup G} (h : H < K) [H.FiniteIndex] :
                          K.index < H.index
                          source
                          theorem AddSubgroup.index_strictAnti {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H < K) [H.FiniteIndex] :
                          K.index < H.index
                          source
                          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
                          source
                          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
                          source
                          instance Subgroup.finiteIndex_normalCore {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] :
                          H.normalCore.FiniteIndex
                          source
                          theorem Subgroup.index_range {G : Type u_1} [Group G] {f : G →* G} [hf : f.ker.FiniteIndex] :
                          f.range.index = Nat.card ↥f.ker
                          source
                          theorem AddSubgroup.index_range {G : Type u_1} [AddGroup G] {f : G →+ G} [hf : f.ker.FiniteIndex] :
                          f.range.index = Nat.card ↥f.ker
                          source
                          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
                          source
                          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
                          source
                          theorem MulAction.index_stabilizer (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (x : X) :
                          (stabilizer G x).index = (orbit G x).ncard
                          source
                          theorem AddAction.index_stabilizer (G : Type u_1) {X : Type u_2} [AddGroup G] [AddAction G X] (x : X) :
                          (stabilizer G x).index = (orbit G x).ncard
                          source
                          theorem MulAction.index_stabilizer_of_transitive (G : Type u_1) {X : Type u_2} [Group G] [MulAction G X] (x : X) [IsPretransitive G X] :
                          (stabilizer G x).index = Nat.card X
                          source
                          theorem AddAction.index_stabilizer_of_transitive (G : Type u_1) {X : Type u_2} [AddGroup G] [AddAction G X] (x : X) [IsPretransitive G X] :
                          (stabilizer G x).index = Nat.card X
                          source
                          theorem MonoidHom.surjective_of_card_ker_le_div {G : Type u_1} {M : Type u_2} [Group G] [Group M] [Finite G] [Finite M] (f : G →* M) (h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M) :
                          Function.Surjective ⇑f
                          source
                          theorem AddMonoidHom.surjective_of_card_ker_le_div {G : Type u_1} {M : Type u_2} [AddGroup G] [AddGroup M] [Finite G] [Finite M] (f : G →+ M) (h : Nat.card ↥f.ker ≤ Nat.card G / Nat.card M) :
                          Function.Surjective ⇑f
                          source
                          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
                          source
                          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
                          source
                          @[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