Subgroups of small index are normal

• Subgroup.normal_of_index_eq_smallest_prime_factor: in a finite group G, a subgroup of index equal to the smallest prime factor of Nat.card G is normal.

• Subgroup.normal_of_index_two: in a group G, a subgroup of index 2 is normal (This does not require G to be finite.)

• Subgroup.isCoatom_of_index_prime: a subgroup of prime index is maximal.

theorem Subgroup.isCoatom_of_index_prime {G : Type u_1} [Group G] {H : Subgroup G} (hH : Nat.Prime H.index) : IsCoatom H

A subgroup of prime index is maximal.

theorem AddSubgroup.isCoatom_of_index_prime {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : Nat.Prime H.index) : IsCoatom H

theorem Subgroup.normal_of_index_eq_one {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.index = 1) : H.Normal

A subgroup of index 1 is normal (does not require finiteness of G)

theorem AddSubgroup.normal_of_index_eq_zero {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.index = 1) : H.Normal

theorem Subgroup.normal_of_index_eq_two {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.index = 2) : H.Normal

A subgroup of index 2 is normal (does not require finiteness of G)

theorem AddSubgroup.normal_of_index_eq_two {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.index = 2) : H.Normal

theorem Subgroup.normal_of_index_eq_minFac_card {G : Type u_1} [Group G] {H : Subgroup G} (hHp : H.index = (Nat.card G).minFac) : H.Normal

A subgroup of a finite group whose index is the smallest prime factor is normal.

Note : if G is infinite, then Nat.card G = 0 and (Nat.card G).minFac = 2

theorem AddSubgroup.index_normalCore_dvd_factorial_index {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [H.FiniteIndex] : H.normalCore.index ∣ H.index.factorial

theorem Subgroup.index_normalCore_dvd_factorial_index {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] : H.normalCore.index ∣ H.index.factorial

theorem Subgroup.index_normalCore_le_factorial_index {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore.index ≤ H.index.factorial

theorem AddSubgroup.index_normalCore_le_factorial_index {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.normalCore.index ≤ H.index.factorial