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
• relindex_mul_index : If H ≤ K, then H.relindex K * K.index = H.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} [AddGroup G] (H : AddSubgroup G) : ℕ

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

Equations

• H.index = Nat.card (G ⧸ H)

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

• H.index = Nat.card (G ⧸ H)

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

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

Equations

• H.relindex K = (H.addSubgroupOf K).index

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

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

Equations

• H.relindex K = (H.subgroupOf K).index

theorem AddSubgroup.index_comap_of_surjective {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] {f : G' →+ G} (hf : Function.Surjective ⇑f) : (AddSubgroup.comap f H).index = H.index

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

theorem AddSubgroup.index_comap {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] (f : G' →+ G) : (AddSubgroup.comap f H).index = H.relindex f.range

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

theorem AddSubgroup.relindex_comap {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] (f : G' →+ G) (K : AddSubgroup G') : (AddSubgroup.comap f H).relindex K = H.relindex (AddSubgroup.map f K)

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)

theorem AddSubgroup.relindex_mul_index {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : H.relindex K * K.index = H.index

theorem Subgroup.relindex_mul_index {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) : H.relindex K * K.index = H.index

theorem AddSubgroup.index_dvd_of_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : K.index ∣ H.index

theorem Subgroup.index_dvd_of_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) : K.index ∣ H.index

theorem AddSubgroup.relindex_dvd_index_of_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H ≤ K) : H.relindex K ∣ H.index

theorem Subgroup.relindex_dvd_index_of_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H ≤ K) : H.relindex K ∣ H.index

theorem AddSubgroup.relindex_addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hKL : K ≤ L) : (H.addSubgroupOf L).relindex (K.addSubgroupOf L) = H.relindex K

theorem Subgroup.relindex_subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hKL : K ≤ L) : (H.subgroupOf L).relindex (K.subgroupOf L) = H.relindex K

theorem AddSubgroup.relindex_mul_relindex {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) (L : AddSubgroup G) (hHK : H ≤ K) (hKL : K ≤ L) : H.relindex K * K.relindex L = H.relindex L

theorem Subgroup.relindex_mul_relindex {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (L : Subgroup G) (hHK : H ≤ K) (hKL : K ≤ L) : H.relindex K * K.relindex L = H.relindex L

theorem AddSubgroup.inf_relindex_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : (H ⊓ K).relindex K = H.relindex K

theorem Subgroup.inf_relindex_right {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : (H ⊓ K).relindex K = H.relindex K

theorem AddSubgroup.inf_relindex_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) : (H ⊓ K).relindex H = K.relindex H

theorem Subgroup.inf_relindex_left {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) : (H ⊓ K).relindex H = K.relindex H

theorem AddSubgroup.relindex_inf_mul_relindex {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) (L : AddSubgroup 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 : Subgroup G) (K : Subgroup G) (L : Subgroup G) : H.relindex (K ⊓ L) * K.relindex L = (H ⊓ K).relindex L

@[simp]

theorem AddSubgroup.relindex_sup_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [K.Normal] : K.relindex (H ⊔ K) = K.relindex H

@[simp]

theorem Subgroup.relindex_sup_right {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) [K.Normal] : K.relindex (H ⊔ K) = K.relindex H

@[simp]

theorem AddSubgroup.relindex_sup_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [K.Normal] : K.relindex (K ⊔ H) = K.relindex H

@[simp]

theorem Subgroup.relindex_sup_left {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) [K.Normal] : K.relindex (K ⊔ H) = K.relindex H

theorem AddSubgroup.relindex_dvd_index_of_normal {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [H.Normal] : H.relindex K ∣ H.index

theorem Subgroup.relindex_dvd_index_of_normal {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) [H.Normal] : H.relindex K ∣ H.index

theorem AddSubgroup.relindex_dvd_of_le_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (L : AddSubgroup G) (hHK : H ≤ K) : K.relindex L ∣ H.relindex L

theorem Subgroup.relindex_dvd_of_le_left {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (L : Subgroup G) (hHK : H ≤ K) : K.relindex L ∣ H.relindex L

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.

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.

theorem AddSubgroup.add_mem_iff_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : H.index = 2) {a : G} {b : G} : a + b ∈ H ↔ (a ∈ H ↔ b ∈ H)

theorem Subgroup.mul_mem_iff_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : H.index = 2) {a : G} {b : G} : a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

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

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

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

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

@[simp]

theorem AddSubgroup.index_top {G : Type u_1} [AddGroup G] : ⊤.index = 1

@[simp]

theorem Subgroup.index_top {G : Type u_1} [Group G] : ⊤.index = 1

@[simp]

theorem AddSubgroup.index_bot {G : Type u_1} [AddGroup G] : ⊥.index = Nat.card G

@[simp]

theorem Subgroup.index_bot {G : Type u_1} [Group G] : ⊥.index = Nat.card G

theorem AddSubgroup.index_bot_eq_card {G : Type u_1} [AddGroup G] [Fintype G] : ⊥.index = Fintype.card G

theorem Subgroup.index_bot_eq_card {G : Type u_1} [Group G] [Fintype G] : ⊥.index = Fintype.card G

@[simp]

theorem AddSubgroup.relindex_top_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊤.relindex H = 1

@[simp]

theorem Subgroup.relindex_top_left {G : Type u_1} [Group G] (H : Subgroup G) : ⊤.relindex H = 1

@[simp]

theorem AddSubgroup.relindex_top_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.relindex ⊤ = H.index

@[simp]

theorem Subgroup.relindex_top_right {G : Type u_1} [Group G] (H : Subgroup G) : H.relindex ⊤ = H.index

@[simp]

theorem AddSubgroup.relindex_bot_left {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : ⊥.relindex H = Nat.card ↥H

@[simp]

theorem Subgroup.relindex_bot_left {G : Type u_1} [Group G] (H : Subgroup G) : ⊥.relindex H = Nat.card ↥H

theorem AddSubgroup.relindex_bot_left_eq_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype ↥H] : ⊥.relindex H = Fintype.card ↥H

theorem Subgroup.relindex_bot_left_eq_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype ↥H] : ⊥.relindex H = Fintype.card ↥H

@[simp]

theorem AddSubgroup.relindex_bot_right {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.relindex ⊥ = 1

@[simp]

theorem Subgroup.relindex_bot_right {G : Type u_1} [Group G] (H : Subgroup G) : H.relindex ⊥ = 1

@[simp]

theorem AddSubgroup.relindex_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.relindex H = 1

@[simp]

theorem Subgroup.relindex_self {G : Type u_1} [Group G] (H : Subgroup G) : H.relindex H = 1

theorem AddSubgroup.index_ker {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) : f.ker.index = Nat.card ↑(Set.range ⇑f)

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)

theorem AddSubgroup.relindex_ker {G : Type u_1} [AddGroup G] {H : Type u_2} [AddGroup H] (f : G →+ H) (K : AddSubgroup G) : f.ker.relindex K = Nat.card ↑(⇑f '' ↑K)

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)

@[simp]

theorem AddSubgroup.card_mul_index {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Nat.card ↥H * H.index = Nat.card G

@[simp]

theorem Subgroup.card_mul_index {G : Type u_1} [Group G] (H : Subgroup G) : Nat.card ↥H * H.index = Nat.card G

theorem AddSubgroup.nat_card_dvd_of_injective {G : Type u_2} {H : Type u_3} [AddGroup G] [AddGroup H] (f : G →+ H) (hf : Function.Injective ⇑f) : Nat.card G ∣ Nat.card H

theorem Subgroup.nat_card_dvd_of_injective {G : Type u_2} {H : Type u_3} [Group G] [Group H] (f : G →* H) (hf : Function.Injective ⇑f) : Nat.card G ∣ Nat.card H

theorem AddSubgroup.nat_card_dvd_of_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem Subgroup.nat_card_dvd_of_le {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) (hHK : H ≤ K) : Nat.card ↥H ∣ Nat.card ↥K

theorem AddSubgroup.nat_card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [AddGroup G] [AddGroup H] (f : G →+ H) (hf : Function.Surjective ⇑f) : Nat.card H ∣ Nat.card G

theorem Subgroup.nat_card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [Group G] [Group H] (f : G →* H) (hf : Function.Surjective ⇑f) : Nat.card H ∣ Nat.card G

theorem AddSubgroup.card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [AddGroup G] [AddGroup H] [Fintype G] [Fintype H] (f : G →+ H) (hf : Function.Surjective ⇑f) : Fintype.card H ∣ Fintype.card G

theorem Subgroup.card_dvd_of_surjective {G : Type u_2} {H : Type u_3} [Group G] [Group H] [Fintype G] [Fintype H] (f : G →* H) (hf : Function.Surjective ⇑f) : Fintype.card H ∣ Fintype.card G

theorem AddSubgroup.index_map {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] (f : G →+ G') : (AddSubgroup.map f H).index = (H ⊔ f.ker).index * f.range.index

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

theorem AddSubgroup.index_map_dvd {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).index ∣ H.index

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

theorem AddSubgroup.dvd_index_map {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf : f.ker ≤ H) : H.index ∣ (AddSubgroup.map f H).index

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

theorem AddSubgroup.index_map_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf1 : Function.Surjective ⇑f) (hf2 : f.ker ≤ H) : (AddSubgroup.map f H).index = H.index

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

theorem AddSubgroup.index_eq_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype (G ⧸ H)] : H.index = Fintype.card (G ⧸ H)

theorem Subgroup.index_eq_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype (G ⧸ H)] : H.index = Fintype.card (G ⧸ H)

theorem AddSubgroup.index_mul_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype G] [hH : Fintype ↥H] : H.index * Fintype.card ↥H = Fintype.card G

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

theorem AddSubgroup.index_dvd_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype G] : H.index ∣ Fintype.card G

theorem Subgroup.index_dvd_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype G] : H.index ∣ Fintype.card G

theorem AddSubgroup.relindex_eq_zero_of_le_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup 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 : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hHK : H ≤ K) (hKL : K.relindex L = 0) : H.relindex L = 0

theorem AddSubgroup.relindex_eq_zero_of_le_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hKL : K ≤ L) (hHK : H.relindex K = 0) : H.relindex L = 0

theorem Subgroup.relindex_eq_zero_of_le_right {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hKL : K ≤ L) (hHK : H.relindex K = 0) : H.relindex L = 0

theorem AddSubgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : H.relindex K = 0) : H.index = 0

theorem Subgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : H.relindex K = 0) : H.index = 0

theorem AddSubgroup.relindex_le_of_le_left {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hHK : H ≤ K) (hHL : H.relindex L ≠ 0) : K.relindex L ≤ H.relindex L

theorem Subgroup.relindex_le_of_le_left {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hHK : H ≤ K) (hHL : H.relindex L ≠ 0) : K.relindex L ≤ H.relindex L

theorem AddSubgroup.relindex_le_of_le_right {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hKL : K ≤ L) (hHL : H.relindex L ≠ 0) : H.relindex K ≤ H.relindex L

theorem Subgroup.relindex_le_of_le_right {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hKL : K ≤ L) (hHL : H.relindex L ≠ 0) : H.relindex K ≤ H.relindex L

theorem AddSubgroup.relindex_ne_zero_trans {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hHK : H.relindex K ≠ 0) (hKL : K.relindex L ≠ 0) : H.relindex L ≠ 0

theorem Subgroup.relindex_ne_zero_trans {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hHK : H.relindex K ≠ 0) (hKL : K.relindex L ≠ 0) : H.relindex L ≠ 0

theorem AddSubgroup.relindex_inf_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} (hH : H.relindex L ≠ 0) (hK : K.relindex L ≠ 0) : (H ⊓ K).relindex L ≠ 0

theorem Subgroup.relindex_inf_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hH : H.relindex L ≠ 0) (hK : K.relindex L ≠ 0) : (H ⊓ K).relindex L ≠ 0

theorem AddSubgroup.index_inf_ne_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0

theorem Subgroup.index_inf_ne_zero {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0

theorem AddSubgroup.relindex_inf_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} {L : AddSubgroup G} : (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

theorem Subgroup.relindex_inf_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} : (H ⊓ K).relindex L ≤ H.relindex L * K.relindex L

theorem AddSubgroup.index_inf_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} : (H ⊓ K).index ≤ H.index * K.index

theorem Subgroup.index_inf_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} : (H ⊓ K).index ≤ H.index * K.index

theorem AddSubgroup.relindex_iInf_ne_zero {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_2} [_hι : Finite ι] {f : ι → AddSubgroup G} (hf : ∀ (i : ι), (f i).relindex L ≠ 0) : (⨅ (i : ι), f i).relindex L ≠ 0

theorem Subgroup.relindex_iInf_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

theorem AddSubgroup.relindex_iInf_le {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_2} [Fintype ι] (f : ι → AddSubgroup G) : (⨅ (i : ι), f i).relindex L ≤ Finset.univ.prod fun (i : ι) => (f i).relindex L

abbrev AddSubgroup.relindex_iInf_le.match_1 {G : Type u_2} [AddGroup G] {L : AddSubgroup G} {ι : Type u_1} [Fintype ι] (f : ι → AddSubgroup G) (motive : (∃ a ∈ Finset.univ, Nat.card (↥L ⧸ (f a).addSubgroupOf L) = 0) → Prop) : ∀ (x : ∃ a ∈ Finset.univ, Nat.card (↥L ⧸ (f a).addSubgroupOf L) = 0), (∀ (i : ι) (_hi : i ∈ Finset.univ) (h : Nat.card (↥L ⧸ (f i).addSubgroupOf L) = 0), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Subgroup.relindex_iInf_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 fun (i : ι) => (f i).relindex L

theorem AddSubgroup.index_iInf_ne_zero {G : Type u_1} [AddGroup G] {ι : Type u_2} [Finite ι] {f : ι → AddSubgroup G} (hf : ∀ (i : ι), (f i).index ≠ 0) : (⨅ (i : ι), f i).index ≠ 0

theorem Subgroup.index_iInf_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

theorem AddSubgroup.index_iInf_le {G : Type u_1} [AddGroup G] {ι : Type u_2} [Fintype ι] (f : ι → AddSubgroup G) : (⨅ (i : ι), f i).index ≤ Finset.univ.prod fun (i : ι) => (f i).index

theorem Subgroup.index_iInf_le {G : Type u_1} [Group G] {ι : Type u_2} [Fintype ι] (f : ι → Subgroup G) : (⨅ (i : ι), f i).index ≤ Finset.univ.prod fun (i : ι) => (f i).index

@[simp]

theorem AddSubgroup.index_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.index = 1 ↔ H = ⊤

@[simp]

theorem Subgroup.index_eq_one {G : Type u_1} [Group G] {H : Subgroup G} : H.index = 1 ↔ H = ⊤

@[simp]

theorem AddSubgroup.relindex_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} : H.relindex K = 1 ↔ K ≤ H

@[simp]

theorem Subgroup.relindex_eq_one {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} : H.relindex K = 1 ↔ K ≤ H

@[simp]

theorem AddSubgroup.card_eq_one {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : Nat.card ↥H = 1 ↔ H = ⊥

@[simp]

theorem Subgroup.card_eq_one {G : Type u_1} [Group G] {H : Subgroup G} : Nat.card ↥H = 1 ↔ H = ⊥

theorem AddSubgroup.index_ne_zero_of_finite {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [hH : Finite (G ⧸ H)] : H.index ≠ 0

theorem Subgroup.index_ne_zero_of_finite {G : Type u_1} [Group G] {H : Subgroup G} [hH : Finite (G ⧸ H)] : H.index ≠ 0

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

• AddSubgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)

theorem AddSubgroup.fintypeOfIndexNeZero.proof_1 {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.index ≠ 0) : Finite (G ⧸ H)

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

• Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)

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

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

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

Typeclass for finite index subgroups.

• finiteIndex : H.index ≠ 0

  The subgroup has finite index

theorem Subgroup.FiniteIndex.finiteIndex {G : Type u_1} [Group G] {H : Subgroup G} [self : H.FiniteIndex] : H.index ≠ 0

The subgroup has finite index

class AddSubgroup.FiniteIndex {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : Prop

Typeclass for finite index subgroups.

• finiteIndex : H.index ≠ 0

  The additive subgroup has finite index

theorem AddSubgroup.FiniteIndex.finiteIndex {G : Type u_2} [AddGroup G] {H : AddSubgroup G} [self : H.FiniteIndex] : H.index ≠ 0

The additive subgroup has finite index

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

• H.fintypeQuotientOfFiniteIndex = AddSubgroup.fintypeOfIndexNeZero ⋯

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

• H.fintypeQuotientOfFiniteIndex = Subgroup.fintypeOfIndexNeZero ⋯

instance AddSubgroup.finite_quotient_of_finiteIndex {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.FiniteIndex] : Finite (G ⧸ H)

Equations

• ⋯ = ⋯

instance Subgroup.finite_quotient_of_finiteIndex {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] : Finite (G ⧸ H)

Equations

• ⋯ = ⋯

theorem AddSubgroup.finiteIndex_of_finite_quotient {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite (G ⧸ H)] : H.FiniteIndex

theorem Subgroup.finiteIndex_of_finite_quotient {G : Type u_1} [Group G] (H : Subgroup G) [Finite (G ⧸ H)] : H.FiniteIndex

@[instance 100]

instance AddSubgroup.finiteIndex_of_finite {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite G] : H.FiniteIndex

Equations

• ⋯ = ⋯

@[instance 100]

instance Subgroup.finiteIndex_of_finite {G : Type u_1} [Group G] (H : Subgroup G) [Finite G] : H.FiniteIndex

Equations

• ⋯ = ⋯

instance AddSubgroup.instFiniteIndexTop {G : Type u_1} [AddGroup G] : ⊤.FiniteIndex

Equations

• ⋯ = ⋯

instance Subgroup.instFiniteIndexTop {G : Type u_1} [Group G] : ⊤.FiniteIndex

Equations

• ⋯ = ⋯

instance AddSubgroup.instFiniteIndexInf {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [H.FiniteIndex] [K.FiniteIndex] : (H ⊓ K).FiniteIndex

Equations

• ⋯ = ⋯

instance Subgroup.instFiniteIndexInf {G : Type u_1} [Group G] (H : Subgroup G) (K : Subgroup G) [H.FiniteIndex] [K.FiniteIndex] : (H ⊓ K).FiniteIndex

Equations

• ⋯ = ⋯

theorem AddSubgroup.finiteIndex_of_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [H.FiniteIndex] (h : H ≤ K) : K.FiniteIndex

theorem Subgroup.finiteIndex_of_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [H.FiniteIndex] (h : H ≤ K) : K.FiniteIndex

instance AddSubgroup.finiteIndex_ker {G : Type u_1} [AddGroup G] {G' : Type u_2} [AddGroup G'] (f : G →+ G') [Finite ↥f.range] : f.ker.FiniteIndex

Equations

• ⋯ = ⋯

instance Subgroup.finiteIndex_ker {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (f : G →* G') [Finite ↥f.range] : f.ker.FiniteIndex

Equations

• ⋯ = ⋯

instance Subgroup.finiteIndex_normalCore {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] : H.normalCore.FiniteIndex

Equations

• ⋯ = ⋯

instance Subgroup.finiteIndex_center (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] [Group.FG G] : (Subgroup.center G).FiniteIndex

Equations

• ⋯ = ⋯

theorem Subgroup.index_center_le_pow (G : Type u_1) [Group G] [Finite ↑(commutatorSet G)] [Group.FG G] : (Subgroup.center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G