mathlib documentation

group_theory.index

Index of a Subgroup #

In this file we define the index of a subgroup, and prove several divisibility properties.

Main definitions #

Main results #

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
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
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
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 add_subgroup.relindex_add_index {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
(H.relindex K) * K.index = H.index
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 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_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) :
(H.relindex K) * K.relindex L = H.relindex L
theorem add_subgroup.relindex_add_relindex {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hHK : H K) (hKL : K L) :
(H.relindex K) * K.relindex L = H.relindex L
@[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
theorem subgroup.index_mul_card {G : Type u_1} [group G] (H : subgroup G) [fintype G] [hH : fintype H] :
theorem add_subgroup.index_add_card {G : Type u_1} [add_group G] (H : add_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] :