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.)

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 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 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