# 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 #

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

# Main results #

• card_mul_index : Nat.card H * H.index = Nat.card G
• index_mul_card : H.index * Fintype.card H = Fintype.card G
• index_dvd_card : H.index ∣ Fintype.card G
• index_eq_mul_of_le : If H ≤ K, then H.index = K.index * (H.subgroupOf K).index
• index_dvd_of_le : If H ≤ K, then K.index ∣ H.index
• relindex_mul_relindex : relindex is multiplicative in towers
noncomputable def AddSubgroup.index {G : Type u_1} [] (H : ) :

The index of a subgroup as a natural number, and returns 0 if the index is infinite.

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

The index of a subgroup as a natural number, and returns 0 if the index is infinite.

Instances For
noncomputable def AddSubgroup.relindex {G : Type u_1} [] (H : ) (K : ) :

The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.

Instances For
noncomputable def Subgroup.relindex {G : Type u_1} [] (H : ) (K : ) :

The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.

Instances For
theorem AddSubgroup.index_comap_of_surjective {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] {f : G' →+ G} (hf : ) :
theorem Subgroup.index_comap_of_surjective {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] {f : G' →* G} (hf : ) :
theorem AddSubgroup.index_comap {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] (f : G' →+ G) :
theorem Subgroup.index_comap {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] (f : G' →* G) :
theorem AddSubgroup.relindex_comap {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] (f : G' →+ G) (K : ) :
theorem Subgroup.relindex_comap {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] (f : G' →* G) (K : Subgroup G') :
=
theorem AddSubgroup.relindex_mul_index {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem Subgroup.relindex_mul_index {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem AddSubgroup.index_dvd_of_le {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem Subgroup.index_dvd_of_le {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem AddSubgroup.relindex_dvd_index_of_le {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem Subgroup.relindex_dvd_index_of_le {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem AddSubgroup.relindex_addSubgroupOf {G : Type u_1} [] {H : } {K : } {L : } (hKL : K L) :
theorem Subgroup.relindex_subgroupOf {G : Type u_1} [] {H : } {K : } {L : } (hKL : K L) :
theorem AddSubgroup.relindex_mul_relindex {G : Type u_1} [] (H : ) (K : ) (L : ) (hHK : H K) (hKL : K L) :
theorem Subgroup.relindex_mul_relindex {G : Type u_1} [] (H : ) (K : ) (L : ) (hHK : H K) (hKL : K L) :
=
theorem AddSubgroup.inf_relindex_right {G : Type u_1} [] (H : ) (K : ) :
theorem Subgroup.inf_relindex_right {G : Type u_1} [] (H : ) (K : ) :
theorem AddSubgroup.inf_relindex_left {G : Type u_1} [] (H : ) (K : ) :
theorem Subgroup.inf_relindex_left {G : Type u_1} [] (H : ) (K : ) :
theorem AddSubgroup.relindex_inf_mul_relindex {G : Type u_1} [] (H : ) (K : ) (L : ) :
theorem Subgroup.relindex_inf_mul_relindex {G : Type u_1} [] (H : ) (K : ) (L : ) :
@[simp]
theorem AddSubgroup.relindex_sup_right {G : Type u_1} [] (H : ) (K : ) :
@[simp]
theorem Subgroup.relindex_sup_right {G : Type u_1} [] (H : ) (K : ) [] :
@[simp]
theorem AddSubgroup.relindex_sup_left {G : Type u_1} [] (H : ) (K : ) :
@[simp]
theorem Subgroup.relindex_sup_left {G : Type u_1} [] (H : ) (K : ) [] :
theorem AddSubgroup.relindex_dvd_index_of_normal {G : Type u_1} [] (H : ) (K : ) :
theorem Subgroup.relindex_dvd_index_of_normal {G : Type u_1} [] (H : ) (K : ) [] :
theorem AddSubgroup.relindex_dvd_of_le_left {G : Type u_1} [] {H : } {K : } (L : ) (hHK : H K) :
theorem Subgroup.relindex_dvd_of_le_left {G : Type u_1} [] {H : } {K : } (L : ) (hHK : H K) :
theorem AddSubgroup.index_eq_two_iff {G : Type u_1} [] {H : } :
a, ∀ (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.index_eq_two_iff {G : Type u_1} [] {H : } :
a, ∀ (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.add_mem_iff_of_index_two {G : Type u_1} [] {H : } (h : ) {a : G} {b : G} :
a + b H (a H b H)
theorem Subgroup.mul_mem_iff_of_index_two {G : Type u_1} [] {H : } (h : ) {a : G} {b : G} :
a * b H (a H b H)
theorem AddSubgroup.add_self_mem_of_index_two {G : Type u_1} [] {H : } (h : ) (a : G) :
a + a H
theorem Subgroup.mul_self_mem_of_index_two {G : Type u_1} [] {H : } (h : ) (a : G) :
a * a H
theorem AddSubgroup.two_smul_mem_of_index_two {G : Type u_1} [] {H : } (h : ) (a : G) :
2 a H
theorem Subgroup.sq_mem_of_index_two {G : Type u_1} [] {H : } (h : ) (a : G) :
a ^ 2 H
@[simp]
theorem AddSubgroup.index_top {G : Type u_1} [] :
@[simp]
theorem Subgroup.index_top {G : Type u_1} [] :
@[simp]
theorem AddSubgroup.index_bot {G : Type u_1} [] :
@[simp]
theorem Subgroup.index_bot {G : Type u_1} [] :
theorem AddSubgroup.index_bot_eq_card {G : Type u_1} [] [] :
theorem Subgroup.index_bot_eq_card {G : Type u_1} [] [] :
@[simp]
theorem AddSubgroup.relindex_top_left {G : Type u_1} [] (H : ) :
@[simp]
theorem Subgroup.relindex_top_left {G : Type u_1} [] (H : ) :
@[simp]
theorem AddSubgroup.relindex_top_right {G : Type u_1} [] (H : ) :
@[simp]
theorem Subgroup.relindex_top_right {G : Type u_1} [] (H : ) :
@[simp]
theorem AddSubgroup.relindex_bot_left {G : Type u_1} [] (H : ) :
= Nat.card { x // x H }
@[simp]
theorem Subgroup.relindex_bot_left {G : Type u_1} [] (H : ) :
= Nat.card { x // x H }
theorem AddSubgroup.relindex_bot_left_eq_card {G : Type u_1} [] (H : ) [Fintype { x // x H }] :
= Fintype.card { x // x H }
theorem Subgroup.relindex_bot_left_eq_card {G : Type u_1} [] (H : ) [Fintype { x // x H }] :
= Fintype.card { x // x H }
@[simp]
theorem AddSubgroup.relindex_bot_right {G : Type u_1} [] (H : ) :
@[simp]
theorem Subgroup.relindex_bot_right {G : Type u_1} [] (H : ) :
@[simp]
theorem AddSubgroup.relindex_self {G : Type u_1} [] (H : ) :
@[simp]
theorem Subgroup.relindex_self {G : Type u_1} [] (H : ) :
= 1
theorem AddSubgroup.index_ker {G : Type u_1} [] {H : Type u_2} [] (f : G →+ H) :
theorem Subgroup.index_ker {G : Type u_1} [] {H : Type u_2} [] (f : G →* H) :
= Nat.card ↑()
theorem AddSubgroup.relindex_ker {G : Type u_1} [] {H : Type u_2} [] (f : G →+ H) (K : ) :
= Nat.card ↑(f '' K)
theorem Subgroup.relindex_ker {G : Type u_1} [] {H : Type u_2} [] (f : G →* H) (K : ) :
= Nat.card ↑(f '' K)
@[simp]
theorem AddSubgroup.card_mul_index {G : Type u_1} [] (H : ) :
Nat.card { x // x H } * =
@[simp]
theorem Subgroup.card_mul_index {G : Type u_1} [] (H : ) :
Nat.card { x // x H } * =
theorem AddSubgroup.nat_card_dvd_of_injective {G : Type u_2} {H : Type u_3} [] [] (f : G →+ H) (hf : ) :
theorem Subgroup.nat_card_dvd_of_injective {G : Type u_2} {H : Type u_3} [] [] (f : G →* H) (hf : ) :
theorem AddSubgroup.nat_card_dvd_of_le {G : Type u_1} [] (H : ) (K : ) (hHK : H K) :
Nat.card { x // x H } Nat.card { x // x K }
theorem Subgroup.nat_card_dvd_of_le {G : Type u_1} [] (H : ) (K : ) (hHK : H K) :
Nat.card { x // x H } Nat.card { x // x K }
theorem AddSubgroup.nat_card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [] [] (f : G →+ H) (hf : ) :
theorem Subgroup.nat_card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [] [] (f : G →* H) (hf : ) :
theorem AddSubgroup.card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [] [] [] [] (f : G →+ H) (hf : ) :
theorem Subgroup.card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [] [] [] [] (f : G →* H) (hf : ) :
theorem AddSubgroup.index_map {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] (f : G →+ G') :
theorem Subgroup.index_map {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] (f : G →* G') :
=
theorem AddSubgroup.index_map_dvd {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf : ) :
theorem Subgroup.index_map_dvd {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] {f : G →* G'} (hf : ) :
theorem AddSubgroup.dvd_index_map {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf : ) :
theorem Subgroup.dvd_index_map {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] {f : G →* G'} (hf : ) :
theorem AddSubgroup.index_map_eq {G : Type u_1} [] (H : ) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf1 : ) (hf2 : ) :
theorem Subgroup.index_map_eq {G : Type u_1} [] (H : ) {G' : Type u_2} [Group G'] {f : G →* G'} (hf1 : ) (hf2 : ) :
theorem AddSubgroup.index_eq_card {G : Type u_1} [] (H : ) [Fintype (G H)] :
theorem Subgroup.index_eq_card {G : Type u_1} [] (H : ) [Fintype (G H)] :
theorem AddSubgroup.index_mul_card {G : Type u_1} [] (H : ) [] [hH : Fintype { x // x H }] :
* Fintype.card { x // x H } =
theorem Subgroup.index_mul_card {G : Type u_1} [] (H : ) [] [hH : Fintype { x // x H }] :
* Fintype.card { x // x H } =
theorem AddSubgroup.index_dvd_card {G : Type u_1} [] (H : ) [] :
theorem Subgroup.index_dvd_card {G : Type u_1} [] (H : ) [] :
theorem AddSubgroup.relindex_eq_zero_of_le_left {G : Type u_1} [] {H : } {K : } {L : } (hHK : H K) (hKL : ) :
theorem Subgroup.relindex_eq_zero_of_le_left {G : Type u_1} [] {H : } {K : } {L : } (hHK : H K) (hKL : = 0) :
= 0
theorem AddSubgroup.relindex_eq_zero_of_le_right {G : Type u_1} [] {H : } {K : } {L : } (hKL : K L) (hHK : ) :
theorem Subgroup.relindex_eq_zero_of_le_right {G : Type u_1} [] {H : } {K : } {L : } (hKL : K L) (hHK : = 0) :
= 0
theorem AddSubgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [] {H : } {K : } (h : ) :
theorem Subgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [] {H : } {K : } (h : = 0) :
theorem AddSubgroup.relindex_le_of_le_left {G : Type u_1} [] {H : } {K : } {L : } (hHK : H K) (hHL : ) :
theorem Subgroup.relindex_le_of_le_left {G : Type u_1} [] {H : } {K : } {L : } (hHK : H K) (hHL : 0) :
theorem AddSubgroup.relindex_le_of_le_right {G : Type u_1} [] {H : } {K : } {L : } (hKL : K L) (hHL : ) :
theorem Subgroup.relindex_le_of_le_right {G : Type u_1} [] {H : } {K : } {L : } (hKL : K L) (hHL : 0) :
theorem AddSubgroup.relindex_ne_zero_trans {G : Type u_1} [] {H : } {K : } {L : } (hHK : ) (hKL : ) :
theorem Subgroup.relindex_ne_zero_trans {G : Type u_1} [] {H : } {K : } {L : } (hHK : 0) (hKL : 0) :
0
theorem AddSubgroup.relindex_inf_ne_zero {G : Type u_1} [] {H : } {K : } {L : } (hH : ) (hK : ) :
theorem Subgroup.relindex_inf_ne_zero {G : Type u_1} [] {H : } {K : } {L : } (hH : 0) (hK : 0) :
theorem AddSubgroup.index_inf_ne_zero {G : Type u_1} [] {H : } {K : } (hH : ) (hK : ) :
theorem Subgroup.index_inf_ne_zero {G : Type u_1} [] {H : } {K : } (hH : ) (hK : ) :
theorem AddSubgroup.relindex_inf_le {G : Type u_1} [] {H : } {K : } {L : } :
theorem Subgroup.relindex_inf_le {G : Type u_1} [] {H : } {K : } {L : } :
theorem AddSubgroup.index_inf_le {G : Type u_1} [] {H : } {K : } :
theorem Subgroup.index_inf_le {G : Type u_1} [] {H : } {K : } :
theorem AddSubgroup.relindex_iInf_ne_zero {G : Type u_1} [] {L : } {ι : Type u_2} [_hι : ] {f : ι} (hf : ∀ (i : ι), AddSubgroup.relindex (f i) L 0) :
AddSubgroup.relindex (⨅ (i : ι), f i) L 0
theorem Subgroup.relindex_iInf_ne_zero {G : Type u_1} [] {L : } {ι : Type u_2} [_hι : ] {f : ι} (hf : ∀ (i : ι), Subgroup.relindex (f i) L 0) :
Subgroup.relindex (⨅ (i : ι), f i) L 0
abbrev AddSubgroup.relindex_iInf_le.match_1 {G : Type u_2} [] {L : } {ι : Type u_1} [] (f : ι) (motive : (a, a Finset.univ Nat.card ({ x // x L } ) = 0) → Prop) :
(x : a, a Finset.univ Nat.card ({ x // x L } ) = 0) → ((i : ι) → (_hi : i Finset.univ) → (h : Nat.card ({ x // x L } ) = 0) → motive (_ : a, a Finset.univ Nat.card ({ x // x L } ) = 0)) → motive x
Instances For
theorem AddSubgroup.relindex_iInf_le {G : Type u_1} [] {L : } {ι : Type u_2} [] (f : ι) :
AddSubgroup.relindex (⨅ (i : ι), f i) L Finset.prod Finset.univ fun i => AddSubgroup.relindex (f i) L
theorem Subgroup.relindex_iInf_le {G : Type u_1} [] {L : } {ι : Type u_2} [] (f : ι) :
Subgroup.relindex (⨅ (i : ι), f i) L Finset.prod Finset.univ fun i => Subgroup.relindex (f i) L
theorem AddSubgroup.index_iInf_ne_zero {G : Type u_1} [] {ι : Type u_2} [] {f : ι} (hf : ∀ (i : ι), AddSubgroup.index (f i) 0) :
AddSubgroup.index (⨅ (i : ι), f i) 0
theorem Subgroup.index_iInf_ne_zero {G : Type u_1} [] {ι : Type u_2} [] {f : ι} (hf : ∀ (i : ι), Subgroup.index (f i) 0) :
Subgroup.index (⨅ (i : ι), f i) 0
theorem AddSubgroup.index_iInf_le {G : Type u_1} [] {ι : Type u_2} [] (f : ι) :
AddSubgroup.index (⨅ (i : ι), f i) Finset.prod Finset.univ fun i => AddSubgroup.index (f i)
theorem Subgroup.index_iInf_le {G : Type u_1} [] {ι : Type u_2} [] (f : ι) :
Subgroup.index (⨅ (i : ι), f i) Finset.prod Finset.univ fun i => Subgroup.index (f i)
@[simp]
theorem AddSubgroup.index_eq_one {G : Type u_1} [] {H : } :
H =
@[simp]
theorem Subgroup.index_eq_one {G : Type u_1} [] {H : } :
H =
@[simp]
theorem AddSubgroup.relindex_eq_one {G : Type u_1} [] {H : } {K : } :
K H
@[simp]
theorem Subgroup.relindex_eq_one {G : Type u_1} [] {H : } {K : } :
= 1 K H
@[simp]
theorem AddSubgroup.card_eq_one {G : Type u_1} [] {H : } :
Nat.card { x // x H } = 1 H =
@[simp]
theorem Subgroup.card_eq_one {G : Type u_1} [] {H : } :
Nat.card { x // x H } = 1 H =
theorem AddSubgroup.index_ne_zero_of_finite {G : Type u_1} [] {H : } [hH : Finite (G H)] :
theorem Subgroup.index_ne_zero_of_finite {G : Type u_1} [] {H : } [hH : Finite (G H)] :
theorem AddSubgroup.fintypeOfIndexNeZero.proof_1 {G : Type u_1} [] {H : } (hH : ) :
Finite (G H)
noncomputable def AddSubgroup.fintypeOfIndexNeZero {G : Type u_1} [] {H : } (hH : ) :
Fintype (G H)

Finite index implies finite quotient.

Instances For
noncomputable def Subgroup.fintypeOfIndexNeZero {G : Type u_1} [] {H : } (hH : ) :
Fintype (G H)

Finite index implies finite quotient.

Instances For
theorem AddSubgroup.one_lt_index_of_ne_top {G : Type u_1} [] {H : } [Finite (G H)] (hH : H ) :
theorem Subgroup.one_lt_index_of_ne_top {G : Type u_1} [] {H : } [Finite (G H)] (hH : H ) :
class Subgroup.FiniteIndex {G : Type u_1} [] (H : ) :
• finiteIndex :

The subgroup has finite index

Typeclass for finite index subgroups.

Instances
class AddSubgroup.FiniteIndex {G : Type u_2} [] (H : ) :
• finiteIndex :

The additive subgroup has finite index

Typeclass for finite index subgroups.

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

A finite index subgroup has finite quotient

Instances For
noncomputable def Subgroup.fintypeQuotientOfFiniteIndex {G : Type u_1} [] (H : ) :
Fintype (G H)

A finite index subgroup has finite quotient.

Instances For
instance Subgroup.finite_quotient_of_finiteIndex {G : Type u_1} [] (H : ) :
Finite (G H)
theorem AddSubgroup.finiteIndex_of_finite_quotient {G : Type u_1} [] (H : ) [Finite (G H)] :
theorem Subgroup.finiteIndex_of_finite_quotient {G : Type u_1} [] (H : ) [Finite (G H)] :
theorem AddSubgroup.finiteIndex_of_finite.proof_1 {G : Type u_1} [] (H : ) [] :
instance AddSubgroup.finiteIndex_of_finite {G : Type u_1} [] (H : ) [] :
instance Subgroup.finiteIndex_of_finite {G : Type u_1} [] (H : ) [] :
theorem AddSubgroup.finiteIndex_of_le {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem Subgroup.finiteIndex_of_le {G : Type u_1} [] {H : } {K : } (h : H K) :
theorem AddSubgroup.finiteIndex_ker.proof_1 {G : Type u_1} [] {G' : Type u_2} [AddGroup G'] (f : G →+ G') [Finite { x // }] :
instance AddSubgroup.finiteIndex_ker {G : Type u_1} [] {G' : Type u_2} [AddGroup G'] (f : G →+ G') [Finite { x // }] :
instance Subgroup.finiteIndex_ker {G : Type u_1} [] {G' : Type u_2} [Group G'] (f : G →* G') [Finite { x // }] :
instance Subgroup.finiteIndex_normalCore {G : Type u_1} [] (H : ) :
instance Subgroup.finiteIndex_center (G : Type u_1) [] [Finite ↑()] [] :
theorem Subgroup.index_center_le_pow (G : Type u_1) [] [Finite ↑()] [] :