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} [AddGroup G] (H : AddSubgroup G) : ℕ

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

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.

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.

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.

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.index (AddSubgroup.comap f H) = AddSubgroup.index H

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.index (Subgroup.comap f H) = Subgroup.index H

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

theorem Subgroup.index_comap {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] (f : G' →* G) : Subgroup.index (Subgroup.comap f H) = Subgroup.relindex H (MonoidHom.range f)

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.relindex (AddSubgroup.comap f H) K = AddSubgroup.relindex H (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.relindex (Subgroup.comap f H) K = Subgroup.relindex H (Subgroup.map f K)

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

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

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

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

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

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

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

theorem Subgroup.relindex_subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} {L : Subgroup G} (hKL : K ≤ L) : Subgroup.relindex (Subgroup.subgroupOf H L) (Subgroup.subgroupOf K L) = Subgroup.relindex H 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) : AddSubgroup.relindex H K * AddSubgroup.relindex K L = AddSubgroup.relindex H 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) : Subgroup.relindex H K * Subgroup.relindex K L = Subgroup.relindex H L

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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) : AddSubgroup.relindex K L ∣ AddSubgroup.relindex H 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) : Subgroup.relindex K L ∣ Subgroup.relindex H L

theorem AddSubgroup.index_eq_two_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : AddSubgroup.index H = 2 ↔ ∃ 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} [Group G] {H : Subgroup G} : Subgroup.index H = 2 ↔ ∃ 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} [AddGroup G] {H : AddSubgroup G} (h : AddSubgroup.index H = 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 : Subgroup.index H = 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 : AddSubgroup.index H = 2) (a : G) : a + a ∈ H

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

theorem AddSubgroup.two_smul_mem_of_index_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (h : AddSubgroup.index H = 2) (a : G) : 2 • a ∈ H

theorem Subgroup.sq_mem_of_index_two {G : Type u_1} [Group G] {H : Subgroup G} (h : Subgroup.index H = 2) (a : G) : a ^ 2 ∈ H

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Subgroup.index_ker {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) : Subgroup.index (MonoidHom.ker f) = 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) : AddSubgroup.relindex (AddMonoidHom.ker f) 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) : Subgroup.relindex (MonoidHom.ker f) K = Nat.card ↑(↑f '' ↑K)

@[simp]

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

@[simp]

theorem Subgroup.card_mul_index {G : Type u_1} [Group G] (H : Subgroup G) : Nat.card { x // x ∈ H } * Subgroup.index H = 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 { x // x ∈ H } ∣ Nat.card { x // x ∈ 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 { x // x ∈ H } ∣ Nat.card { x // x ∈ 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.index (AddSubgroup.map f H) = AddSubgroup.index (H ⊔ AddMonoidHom.ker f) * AddSubgroup.index (AddMonoidHom.range f)

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

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.index (AddSubgroup.map f H) ∣ AddSubgroup.index H

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.index (Subgroup.map f H) ∣ Subgroup.index H

theorem AddSubgroup.dvd_index_map {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] {f : G →+ G'} (hf : AddMonoidHom.ker f ≤ H) : AddSubgroup.index H ∣ AddSubgroup.index (AddSubgroup.map f 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 : MonoidHom.ker f ≤ H) : Subgroup.index H ∣ Subgroup.index (Subgroup.map f H)

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 : AddMonoidHom.ker f ≤ H) : AddSubgroup.index (AddSubgroup.map f H) = AddSubgroup.index 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 : MonoidHom.ker f ≤ H) : Subgroup.index (Subgroup.map f H) = Subgroup.index H

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

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

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

theorem Subgroup.index_mul_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype G] [hH : Fintype { x // x ∈ H }] : Subgroup.index H * Fintype.card { x // x ∈ H } = Fintype.card G

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

theorem Subgroup.index_dvd_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype G] : Subgroup.index H ∣ 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 : AddSubgroup.relindex K L = 0) : AddSubgroup.relindex H 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 : Subgroup.relindex K L = 0) : Subgroup.relindex H 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 : AddSubgroup.relindex H K = 0) : AddSubgroup.relindex H 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 : Subgroup.relindex H K = 0) : Subgroup.relindex H L = 0

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

theorem Subgroup.index_eq_zero_of_relindex_eq_zero {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (h : Subgroup.relindex H K = 0) : Subgroup.index H = 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 : AddSubgroup.relindex H L ≠ 0) : AddSubgroup.relindex K L ≤ AddSubgroup.relindex H 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 : Subgroup.relindex H L ≠ 0) : Subgroup.relindex K L ≤ Subgroup.relindex H 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 : AddSubgroup.relindex H L ≠ 0) : AddSubgroup.relindex H K ≤ AddSubgroup.relindex H 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 : Subgroup.relindex H L ≠ 0) : Subgroup.relindex H K ≤ Subgroup.relindex H L

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

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

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

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

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

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

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

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

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

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

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 : ι), AddSubgroup.relindex (f i) L ≠ 0) : AddSubgroup.relindex (⨅ (i : ι), f i) 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 : ι), Subgroup.relindex (f i) L ≠ 0) : Subgroup.relindex (⨅ (i : ι), f i) L ≠ 0

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, a ∈ Finset.univ ∧ Nat.card ({ x // x ∈ L } ⧸ AddSubgroup.addSubgroupOf (f a) L) = 0) → Prop) : (x : ∃ a, a ∈ Finset.univ ∧ Nat.card ({ x // x ∈ L } ⧸ AddSubgroup.addSubgroupOf (f a) L) = 0) → ((i : ι) → (_hi : i ∈ Finset.univ) → (h : Nat.card ({ x // x ∈ L } ⧸ AddSubgroup.addSubgroupOf (f i) L) = 0) → motive (_ : ∃ a, a ∈ Finset.univ ∧ Nat.card ({ x // x ∈ L } ⧸ AddSubgroup.addSubgroupOf (f a) L) = 0)) → motive x

theorem AddSubgroup.relindex_iInf_le {G : Type u_1} [AddGroup G] {L : AddSubgroup G} {ι : Type u_2} [Fintype ι] (f : ι → AddSubgroup G) : 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} [Group G] {L : Subgroup G} {ι : Type u_2} [Fintype ι] (f : ι → Subgroup G) : 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} [AddGroup G] {ι : Type u_2} [Finite ι] {f : ι → AddSubgroup G} (hf : ∀ (i : ι), AddSubgroup.index (f i) ≠ 0) : AddSubgroup.index (⨅ (i : ι), f i) ≠ 0

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

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

theorem Subgroup.index_iInf_le {G : Type u_1} [Group G] {ι : Type u_2} [Fintype ι] (f : ι → Subgroup G) : 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} [AddGroup G] {H : AddSubgroup G} : AddSubgroup.index H = 1 ↔ H = ⊤

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

noncomputable def AddSubgroup.fintypeOfIndexNeZero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : AddSubgroup.index H ≠ 0) : Fintype (G ⧸ H)

Finite index implies finite quotient.

noncomputable def Subgroup.fintypeOfIndexNeZero {G : Type u_1} [Group G] {H : Subgroup G} (hH : Subgroup.index H ≠ 0) : Fintype (G ⧸ H)

Finite index implies finite quotient.

theorem AddSubgroup.one_lt_index_of_ne_top {G : Type u_1} [AddGroup G] {H : AddSubgroup G} [Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < AddSubgroup.index H

theorem Subgroup.one_lt_index_of_ne_top {G : Type u_1} [Group G] {H : Subgroup G} [Finite (G ⧸ H)] (hH : H ≠ ⊤) : 1 < Subgroup.index H

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

• finiteIndex : Subgroup.index H ≠ 0

  The subgroup has finite index

Typeclass for finite index subgroups.

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

• finiteIndex : AddSubgroup.index H ≠ 0

  The additive subgroup has finite index

Typeclass for finite index subgroups.

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

A finite index subgroup has finite quotient

noncomputable def Subgroup.fintypeQuotientOfFiniteIndex {G : Type u_1} [Group G] (H : Subgroup G) [Subgroup.FiniteIndex H] : Fintype (G ⧸ H)

A finite index subgroup has finite quotient.

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

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

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

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

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

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

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

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

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

theorem AddSubgroup.instFiniteIndexTopAddSubgroupInstTopAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] : AddSubgroup.FiniteIndex ⊤

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

theorem AddSubgroup.instFiniteIndexInfAddSubgroupInstInfAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (K : AddSubgroup G) [AddSubgroup.FiniteIndex H] [AddSubgroup.FiniteIndex K] : AddSubgroup.FiniteIndex (H ⊓ K)

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

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

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

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

theorem AddSubgroup.finiteIndex_ker.proof_1 {G : Type u_1} [AddGroup G] {G' : Type u_2} [AddGroup G'] (f : G →+ G') [Finite { x // x ∈ AddMonoidHom.range f }] : AddSubgroup.FiniteIndex (AddMonoidHom.ker f)

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

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

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

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

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