mathlib3 documentation

group_theory.index

Index of a Subgroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Equations
source
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
source
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
source
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
source
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) :
(subgroup.comap f H).index = H.index
source
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) :
(add_subgroup.comap f H).index = H.index
source
theorem subgroup.index_comap {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] (f : G' →* G) :
(subgroup.comap f H).index = H.relindex f.range
source
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) :
(add_subgroup.comap f H).index = H.relindex f.range
source
theorem add_subgroup.relindex_comap {G : Type u_1} [add_group G] (H : add_subgroup G) {G' : Type u_2} [add_group G'] (f : G' →+ G) (K : add_subgroup G') :
(add_subgroup.comap f H).relindex K = H.relindex (add_subgroup.map f K)
source
theorem subgroup.relindex_comap {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] (f : G' →* G) (K : subgroup G') :
(subgroup.comap f H).relindex K = H.relindex (subgroup.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 add_subgroup.relindex_mul_index {G : Type u_1} [add_group G] {H K : add_subgroup 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 add_subgroup.index_dvd_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :
K.index ∣ H.index
source
theorem add_subgroup.relindex_dvd_index_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :
H.relindex K ∣ 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 add_subgroup.relindex_add_subgroup_of {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hKL : K ≤ L) :
(H.add_subgroup_of L).relindex (K.add_subgroup_of L) = H.relindex K
source
theorem subgroup.relindex_subgroup_of {G : Type u_1} [group G] {H K L : subgroup G} (hKL : K ≤ L) :
(H.subgroup_of L).relindex (K.subgroup_of 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 add_subgroup.relindex_mul_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
source
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
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 subgroup.inf_relindex_left {G : Type u_1} [group G] (H K : subgroup G) :
(H ⊓ K).relindex H = K.relindex H
source
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
source
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
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
@[simp]
theorem add_subgroup.relindex_sup_right {G : Type u_1} [add_group G] (H K : add_subgroup G) [K.normal] :
K.relindex (H ⊔ K) = K.relindex H
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 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 add_subgroup.relindex_sup_left {G : Type u_1} [add_group G] (H K : add_subgroup G) [K.normal] :
K.relindex (K ⊔ H) = K.relindex H
source
theorem add_subgroup.relindex_dvd_index_of_normal {G : Type u_1} [add_group G] (H K : add_subgroup G) [H.normal] :
H.relindex K ∣ H.index
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 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) :
K.relindex L ∣ H.relindex L
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 add_subgroup.index_eq_two_iff {G : Type u_1} [add_group G] {H : add_subgroup 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.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 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 add_subgroup.add_mem_iff_of_index_two {G : Type u_1} [add_group G] {H : add_subgroup G} (h : H.index = 2) {a b : G} :
a + b ∈ H ↔ (a ∈ H ↔ b ∈ H)
source
theorem add_subgroup.add_self_mem_of_index_two {G : Type u_1} [add_group G] {H : add_subgroup G} (h : H.index = 2) (a : G) :
a + a ∈ 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 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 add_subgroup.two_smul_mem_of_index_two {G : Type u_1} [add_group G] {H : add_subgroup G} (h : H.index = 2) (a : G) :
2 • a ∈ H
source
@[simp]
theorem add_subgroup.index_top {G : Type u_1} [add_group G] :
⊤.index = 1
source
@[simp]
theorem subgroup.index_top {G : Type u_1} [group G] :
⊤.index = 1
source
@[simp]
theorem subgroup.index_bot {G : Type u_1} [group G] :
⊥.index = nat.card G
source
@[simp]
theorem add_subgroup.index_bot {G : Type u_1} [add_group G] :
⊥.index = nat.card G
source
theorem add_subgroup.index_bot_eq_card {G : Type u_1} [add_group G] [fintype G] :
⊥.index = fintype.card G
source
theorem subgroup.index_bot_eq_card {G : Type u_1} [group G] [fintype G] :
⊥.index = fintype.card G
source
@[simp]
theorem add_subgroup.relindex_top_left {G : Type u_1} [add_group G] (H : add_subgroup G) :
⊤.relindex H = 1
source
@[simp]
theorem subgroup.relindex_top_left {G : Type u_1} [group G] (H : subgroup 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 add_subgroup.relindex_top_right {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex ⊤ = H.index
source
@[simp]
theorem add_subgroup.relindex_bot_left {G : Type u_1} [add_group G] (H : add_subgroup G) :
⊥.relindex H = nat.card ↥H
source
@[simp]
theorem subgroup.relindex_bot_left {G : Type u_1} [group G] (H : subgroup G) :
⊥.relindex H = nat.card ↥H
source
theorem subgroup.relindex_bot_left_eq_card {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] :
⊥.relindex H = fintype.card ↥H
source
theorem add_subgroup.relindex_bot_left_eq_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] :
⊥.relindex H = fintype.card ↥H
source
@[simp]
theorem subgroup.relindex_bot_right {G : Type u_1} [group G] (H : subgroup G) :
H.relindex ⊥ = 1
source
@[simp]
theorem add_subgroup.relindex_bot_right {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex ⊥ = 1
source
@[simp]
theorem add_subgroup.relindex_self {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex H = 1
source
@[simp]
theorem subgroup.relindex_self {G : Type u_1} [group G] (H : subgroup G) :
H.relindex H = 1
source
theorem add_subgroup.index_ker {G : Type u_1} [add_group G] {H : Type u_2} [add_group H] (f : G →+ H) :
f.ker.index = nat.card ↥(set.range ⇑f)
source
theorem subgroup.index_ker {G : Type u_1} [group G] {H : Type u_2} [group H] (f : G →* H) :
f.ker.index = nat.card ↥(set.range ⇑f)
source
theorem subgroup.relindex_ker {G : Type u_1} [group G] {H : Type u_2} [group H] (f : G →* H) (K : subgroup G) :
f.ker.relindex K = nat.card ↥(⇑f '' ↑K)
source
theorem add_subgroup.relindex_ker {G : Type u_1} [add_group G] {H : Type u_2} [add_group H] (f : G →+ H) (K : add_subgroup G) :
f.ker.relindex K = nat.card ↥(⇑f '' ↑K)
source
@[simp]
theorem add_subgroup.card_mul_index {G : Type u_1} [add_group G] (H : add_subgroup G) :
nat.card ↥H * H.index = nat.card G
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
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) :
nat.card G ∣ nat.card H
source
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) :
nat.card G ∣ nat.card H
source
theorem subgroup.nat_card_dvd_of_le {G : Type u_1} [group G] (H K : subgroup G) (hHK : H ≤ K) :
nat.card ↥H ∣ nat.card ↥K
source
theorem add_subgroup.nat_card_dvd_of_le {G : Type u_1} [add_group G] (H K : add_subgroup G) (hHK : H ≤ K) :
nat.card ↥H ∣ nat.card ↥K
source
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) :
nat.card H ∣ nat.card G
source
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) :
nat.card H ∣ nat.card G
source
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) :
fintype.card H ∣ fintype.card G
source
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) :
fintype.card H ∣ fintype.card G
source
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') :
(add_subgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
source
theorem subgroup.index_map {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] (f : G →* G') :
(subgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
source
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) :
(add_subgroup.map f H).index ∣ H.index
source
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) :
(subgroup.map f H).index ∣ H.index
source
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) :
H.index ∣ (add_subgroup.map f H).index
source
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) :
H.index ∣ (subgroup.map f H).index
source
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) :
(add_subgroup.map f H).index = H.index
source
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) :
(subgroup.map f H).index = H.index
source
theorem subgroup.index_eq_card {G : Type u_1} [group G] (H : subgroup G) [fintype (G ⧸ H)] :
H.index = fintype.card (G ⧸ H)
source
theorem add_subgroup.index_eq_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype (G ⧸ H)] :
H.index = fintype.card (G ⧸ H)
source
theorem subgroup.index_mul_card {G : Type u_1} [group G] (H : subgroup G) [fintype G] [hH : fintype ↥H] :
H.index * fintype.card ↥H = fintype.card G
source
theorem add_subgroup.index_mul_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype G] [hH : fintype ↥H] :
H.index * fintype.card ↥H = fintype.card G
source
theorem subgroup.index_dvd_card {G : Type u_1} [group G] (H : subgroup G) [fintype G] :
H.index ∣ fintype.card G
source
theorem add_subgroup.index_dvd_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype G] :
H.index ∣ fintype.card G
source
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
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 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 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
source
theorem add_subgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H.relindex K = 0) :
H.index = 0
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 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 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) :
K.relindex L ≤ H.relindex L
source
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) :
H.relindex K ≤ 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 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) :
H.relindex L ≠ 0
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 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 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
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 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
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 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
source
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
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 subgroup.relindex_infi_ne_zero {G : Type u_1} [group G] {L : subgroup G} {ι : Type u_2} [hι : finite ι] {f : ι → subgroup G} (hf : ∀ (i : ι), (f i).relindex L ≠ 0) :
(⨅ (i : ι), f i).relindex L ≠ 0
source
theorem add_subgroup.relindex_infi_ne_zero {G : Type u_1} [add_group G] {L : add_subgroup G} {ι : Type u_2} [hι : finite ι] {f : ι → add_subgroup G} (hf : ∀ (i : ι), (f i).relindex L ≠ 0) :
(⨅ (i : ι), f i).relindex L ≠ 0
source
theorem subgroup.relindex_infi_le {G : Type u_1} [group G] {L : subgroup G} {ι : Type u_2} [fintype ι] (f : ι → subgroup G) :
(⨅ (i : ι), f i).relindex L ≤ finset.univ.prod (λ (i : ι), (f i).relindex L)
source
theorem add_subgroup.relindex_infi_le {G : Type u_1} [add_group G] {L : add_subgroup G} {ι : Type u_2} [fintype ι] (f : ι → add_subgroup G) :
(⨅ (i : ι), f i).relindex L ≤ finset.univ.prod (λ (i : ι), (f i).relindex L)
source
theorem subgroup.index_infi_ne_zero {G : Type u_1} [group G] {ι : Type u_2} [finite ι] {f : ι → subgroup G} (hf : ∀ (i : ι), (f i).index ≠ 0) :
(⨅ (i : ι), f i).index ≠ 0
source
theorem add_subgroup.index_infi_ne_zero {G : Type u_1} [add_group G] {ι : Type u_2} [finite ι] {f : ι → add_subgroup G} (hf : ∀ (i : ι), (f i).index ≠ 0) :
(⨅ (i : ι), f i).index ≠ 0
source
theorem add_subgroup.index_infi_le {G : Type u_1} [add_group G] {ι : Type u_2} [fintype ι] (f : ι → add_subgroup G) :
(⨅ (i : ι), f i).index ≤ finset.univ.prod (λ (i : ι), (f i).index)
source
theorem subgroup.index_infi_le {G : Type u_1} [group G] {ι : Type u_2} [fintype ι] (f : ι → subgroup G) :
(⨅ (i : ι), f i).index ≤ finset.univ.prod (λ (i : ι), (f i).index)
source
@[simp]
theorem add_subgroup.index_eq_one {G : Type u_1} [add_group G] {H : add_subgroup G} :
H.index = 1 ↔ H = ⊤
source
@[simp]
theorem subgroup.index_eq_one {G : Type u_1} [group G] {H : subgroup 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 add_subgroup.relindex_eq_one {G : Type u_1} [add_group G] {H K : add_subgroup G} :
H.relindex K = 1 ↔ K ≤ H
source
@[simp]
theorem add_subgroup.card_eq_one {G : Type u_1} [add_group G] {H : add_subgroup G} :
nat.card ↥H = 1 ↔ H = ⊥
source
@[simp]
theorem subgroup.card_eq_one {G : Type u_1} [group G] {H : subgroup G} :
nat.card ↥H = 1 ↔ H = ⊥
source
theorem add_subgroup.index_ne_zero_of_finite {G : Type u_1} [add_group G] {H : add_subgroup G} [hH : finite (G ⧸ H)] :
H.index ≠ 0
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
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
source
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
source
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
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
@[class]
structure subgroup.finite_index {G : Type u_1} [group G] (H : subgroup G) :
Prop

Typeclass for finite index subgroups.

Instances of this typeclass
source
@[class]
structure add_subgroup.finite_index {G : Type u_2} [add_group G] (H : add_subgroup G) :
Prop

Typeclass for finite index subgroups.

Instances of this typeclass
source
noncomputable def subgroup.fintype_quotient_of_finite_index {G : Type u_1} [group G] (H : subgroup G) [H.finite_index] :
fintype (G ⧸ H)

A finite index subgroup has finite quotient.

Equations
source
noncomputable def add_subgroup.fintype_quotient_of_finite_index {G : Type u_1} [add_group G] (H : add_subgroup G) [H.finite_index] :
fintype (G ⧸ H)

A finite index subgroup has finite quotient

Equations
source
@[protected, instance]
def add_subgroup.finite_quotient_of_finite_index {G : Type u_1} [add_group G] (H : add_subgroup G) [H.finite_index] :
finite (G ⧸ H)
source
@[protected, instance]
def subgroup.finite_quotient_of_finite_index {G : Type u_1} [group G] (H : subgroup G) [H.finite_index] :
finite (G ⧸ H)
source
theorem add_subgroup.finite_index_of_finite_quotient {G : Type u_1} [add_group G] (H : add_subgroup G) [finite (G ⧸ H)] :
H.finite_index
source
theorem subgroup.finite_index_of_finite_quotient {G : Type u_1} [group G] (H : subgroup G) [finite (G ⧸ H)] :
H.finite_index
source
@[protected, instance]
def add_subgroup.finite_index_of_finite {G : Type u_1} [add_group G] (H : add_subgroup G) [finite G] :
H.finite_index
source
@[protected, instance]
def subgroup.finite_index_of_finite {G : Type u_1} [group G] (H : subgroup G) [finite G] :
H.finite_index
source
@[protected, instance]
def subgroup.has_top.top.finite_index {G : Type u_1} [group G] :
⊤.finite_index
source
@[protected, instance]
def add_subgroup.has_top.top.finite_index {G : Type u_1} [add_group G] :
⊤.finite_index
source
@[protected, instance]
def add_subgroup.has_inf.inf.finite_index {G : Type u_1} [add_group G] (H K : add_subgroup G) [H.finite_index] [K.finite_index] :
(H ⊓ K).finite_index
source
@[protected, instance]
def subgroup.has_inf.inf.finite_index {G : Type u_1} [group G] (H K : subgroup G) [H.finite_index] [K.finite_index] :
(H ⊓ K).finite_index
source
theorem subgroup.finite_index_of_le {G : Type u_1} [group G] {H K : subgroup G} [H.finite_index] (h : H ≤ K) :
K.finite_index
source
theorem add_subgroup.finite_index_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} [H.finite_index] (h : H ≤ K) :
K.finite_index
source
@[protected, instance]
def subgroup.finite_index_ker {G : Type u_1} [group G] {G' : Type u_2} [group G'] (f : G →* G') [finite ↥(f.range)] :
f.ker.finite_index
source
@[protected, instance]
def add_subgroup.finite_index_ker {G : Type u_1} [add_group G] {G' : Type u_2} [add_group G'] (f : G →+ G') [finite ↥(f.range)] :
f.ker.finite_index
source
@[protected, instance]
def subgroup.finite_index_normal_core {G : Type u_1} [group G] (H : subgroup G) [H.finite_index] :
H.normal_core.finite_index
source
@[protected, instance]
def subgroup.finite_index_center (G : Type u_1) [group G] [finite ↥(commutator_set G)] [group.fg G] :
(subgroup.center G).finite_index
source
theorem subgroup.index_center_le_pow (G : Type u_1) [group G] [finite ↥(commutator_set G)] [group.fg G] :
(subgroup.center G).index ≤ nat.card ↥(commutator_set G) ^ group.rank G