mathlib documentation

group_theory.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, and returns 0 if the index is infinite.

Equations
noncomputable def add_subgroup.index {G : Type u_1} [add_group G] (H : add_subgroup G) :

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

Equations
noncomputable def subgroup.relindex {G : Type u_1} [group G] (H K : subgroup G) :

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

Equations
noncomputable def add_subgroup.relindex {G : Type u_1} [add_group G] (H K : add_subgroup G) :

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

Equations
theorem subgroup.index_comap_of_surjective {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] {f : G' →* G} (hf : function.surjective f) :
theorem add_subgroup.index_comap_of_surjective {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] {f : G' →+ G} (hf : function.surjective f) :
theorem subgroup.index_comap {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] (f : G' →* G) :
theorem add_subgroup.index_comap {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] (f : G' →+ G) :
theorem subgroup.relindex_mul_index {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :
theorem add_subgroup.relindex_mul_index {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
theorem subgroup.index_dvd_of_le {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :
theorem add_subgroup.index_dvd_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
theorem add_subgroup.relindex_dvd_index_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
theorem subgroup.relindex_dvd_index_of_le {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :
theorem add_subgroup.relindex_add_subgroup_of {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hKL : K L) :
theorem subgroup.relindex_subgroup_of {G : Type u_1} [group G] {H K L : subgroup G} (hKL : K L) :
theorem subgroup.relindex_mul_relindex {G : Type u_1} [group G] (H K L : subgroup G) (hHK : H K) (hKL : K L) :
theorem add_subgroup.relindex_mul_relindex {G : Type u_1} [add_group G] (H K L : add_subgroup G) (hHK : H K) (hKL : K L) :
theorem add_subgroup.inf_relindex_right {G : Type u_1} [add_group G] (H K : add_subgroup G) :
(H K).relindex K = H.relindex K
theorem subgroup.inf_relindex_right {G : Type u_1} [group G] (H K : subgroup 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 add_subgroup.inf_relindex_left {G : Type u_1} [add_group G] (H K : add_subgroup G) :
(H K).relindex H = K.relindex H
theorem add_subgroup.relindex_inf_mul_relindex {G : Type u_1} [add_group G] (H K L : add_subgroup G) :
H.relindex (K L) * K.relindex L = (H K).relindex L
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 add_subgroup.inf_relindex_eq_relindex_sup {G : Type u_1} [add_group G] (H K : add_subgroup G) [K.normal] :
(H K).relindex H = K.relindex (H K)
theorem subgroup.inf_relindex_eq_relindex_sup {G : Type u_1} [group G] (H K : subgroup G) [K.normal] :
(H K).relindex H = K.relindex (H K)
theorem add_subgroup.relindex_eq_relindex_sup {G : Type u_1} [add_group G] (H K : add_subgroup G) [K.normal] :
K.relindex H = K.relindex (H K)
theorem subgroup.relindex_eq_relindex_sup {G : Type u_1} [group G] (H K : subgroup G) [K.normal] :
K.relindex H = K.relindex (H K)
theorem subgroup.relindex_dvd_index_of_normal {G : Type u_1} [group G] (H K : subgroup G) [H.normal] :
theorem add_subgroup.relindex_dvd_of_le_left {G : Type u_1} [add_group G] {H K : add_subgroup G} (L : add_subgroup G) (hHK : H K) :
theorem subgroup.relindex_dvd_of_le_left {G : Type u_1} [group G] {H K : subgroup G} (L : subgroup G) (hHK : H K) :
@[simp]
theorem add_subgroup.index_top {G : Type u_1} [add_group G] :
@[simp]
theorem subgroup.index_top {G : Type u_1} [group G] :
@[simp]
theorem subgroup.index_bot {G : Type u_1} [group G] :
@[simp]
theorem add_subgroup.index_bot {G : Type u_1} [add_group G] :
theorem subgroup.index_bot_eq_card {G : Type u_1} [group G] [fintype G] :
@[simp]
theorem add_subgroup.relindex_top_left {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem subgroup.relindex_top_left {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem subgroup.relindex_top_right {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.relindex_top_right {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem add_subgroup.relindex_bot_left {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem subgroup.relindex_bot_left {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem subgroup.relindex_bot_right {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.relindex_bot_right {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem add_subgroup.relindex_self {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex H = 1
@[simp]
theorem subgroup.relindex_self {G : Type u_1} [group G] (H : subgroup G) :
H.relindex H = 1
@[simp]
theorem add_subgroup.card_mul_index {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem subgroup.card_mul_index {G : Type u_1} [group G] (H : subgroup G) :
theorem subgroup.nat_card_dvd_of_injective {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (hf : function.injective f) :
theorem add_subgroup.nat_card_dvd_of_injective {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (hf : function.injective f) :
theorem subgroup.nat_card_dvd_of_surjective {G : Type u_1} {H : Type u_2} [group G] [group H] (f : G →* H) (hf : function.surjective f) :
theorem add_subgroup.nat_card_dvd_of_surjective {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (hf : function.surjective f) :
theorem add_subgroup.card_dvd_of_surjective {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] [fintype G] [fintype H] (f : G →+ H) (hf : function.surjective f) :
theorem subgroup.card_dvd_of_surjective {G : Type u_1} {H : Type u_2} [group G] [group H] [fintype G] [fintype H] (f : G →* H) (hf : function.surjective f) :
theorem add_subgroup.index_map {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] (f : G →+ G') :
theorem subgroup.index_map {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] (f : G →* G') :
theorem add_subgroup.index_map_dvd {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] {f : G →+ G'} (hf : function.surjective f) :
theorem subgroup.index_map_dvd {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] {f : G →* G'} (hf : function.surjective f) :
theorem add_subgroup.dvd_index_map {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] {f : G →+ G'} (hf : f.ker H) :
theorem subgroup.dvd_index_map {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] {f : G →* G'} (hf : f.ker H) :
theorem add_subgroup.index_map_eq {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] {f : G →+ G'} (hf1 : function.surjective f) (hf2 : f.ker H) :
theorem subgroup.index_map_eq {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] {f : G →* G'} (hf1 : function.surjective f) (hf2 : f.ker H) :
theorem subgroup.index_eq_card {G : Type u_1} [group G] (H : subgroup G) [fintype (G H)] :
theorem add_subgroup.index_eq_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype (G H)] :
theorem subgroup.index_mul_card {G : Type u_1} [group G] (H : subgroup G) [fintype G] [hH : fintype H] :
theorem subgroup.index_dvd_card {G : Type u_1} [group G] (H : subgroup G) [fintype G] :
theorem add_subgroup.index_dvd_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype G] :
theorem add_subgroup.relindex_eq_zero_of_le_left {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hHK : H K) (hKL : K.relindex L = 0) :
H.relindex L = 0
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 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 add_subgroup.relindex_eq_zero_of_le_right {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hKL : K L) (hHK : H.relindex K = 0) :
H.relindex L = 0
theorem subgroup.relindex_le_of_le_left {G : Type u_1} [group G] {H K L : subgroup G} (hHK : H K) (hHL : H.relindex L 0) :
theorem add_subgroup.relindex_le_of_le_left {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hHK : H K) (hHL : H.relindex L 0) :
theorem add_subgroup.relindex_le_of_le_right {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hKL : K L) (hHL : H.relindex L 0) :
theorem subgroup.relindex_le_of_le_right {G : Type u_1} [group G] {H K L : subgroup G} (hKL : K L) (hHL : H.relindex L 0) :
theorem add_subgroup.relindex_ne_zero_trans {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hHK : H.relindex K 0) (hKL : K.relindex L 0) :
theorem subgroup.relindex_ne_zero_trans {G : Type u_1} [group G] {H K L : subgroup G} (hHK : H.relindex K 0) (hKL : K.relindex L 0) :
theorem 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 add_subgroup.relindex_inf_ne_zero {G : Type u_1} [add_group G] {H K L : add_subgroup 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 add_subgroup.index_inf_ne_zero {G : Type u_1} [add_group G] {H K : add_subgroup 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 add_subgroup.relindex_inf_le {G : Type u_1} [add_group G] {H K L : add_subgroup G} :
(H K).relindex L H.relindex L * K.relindex L
theorem add_subgroup.index_inf_le {G : Type u_1} [add_group G] {H K : add_subgroup G} :
(H K).index H.index * K.index
theorem subgroup.index_inf_le {G : Type u_1} [group G] {H K : subgroup G} :
(H K).index H.index * K.index
@[simp]
theorem add_subgroup.index_eq_one {G : Type u_1} [add_group G] {H : add_subgroup G} :
H.index = 1 H =
@[simp]
theorem subgroup.index_eq_one {G : Type u_1} [group G] {H : subgroup G} :
H.index = 1 H =
theorem add_subgroup.index_ne_zero_of_finite {G : Type u_1} [add_group G] {H : add_subgroup G} [hH : finite (G H)] :
theorem subgroup.index_ne_zero_of_finite {G : Type u_1} [group G] {H : subgroup G} [hH : finite (G H)] :
noncomputable def subgroup.fintype_of_index_ne_zero {G : Type u_1} [group G] {H : subgroup G} (hH : H.index 0) :
fintype (G H)

Finite index implies finite quotient.

Equations
noncomputable def add_subgroup.fintype_of_index_ne_zero {G : Type u_1} [add_group G] {H : add_subgroup G} (hH : H.index 0) :
fintype (G H)

Finite index implies finite quotient.

Equations
theorem add_subgroup.one_lt_index_of_ne_top {G : Type u_1} [add_group G] {H : add_subgroup G} [finite (G H)] (hH : H ) :
1 < H.index
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