English
A subgroup whose index equals the smallest prime factor of |G| is normal; similarly for infinite G with minFac=2.
Русский
Подгруппа с индексом, равным наименьшему простому делителю |G|, нормальна; аналогично для бесконечных групп с minFac=2.
LaTeX
$$H.index = (|G|).minFac → H.Normal$$
Lean4
/-- 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 normal_of_index_eq_minFac_card (hHp : H.index = (Nat.card G).minFac) : H.Normal :=
by
by_cases hG0 : Nat.card G = 0
· rw [hG0, minFac_zero] at hHp
exact normal_of_index_eq_two hHp
by_cases hG1 : Nat.card G = 1
· rw [hG1, minFac_one] at hHp
exact normal_of_index_eq_one hHp
suffices H.normalCore.relIndex H = 1 by
convert H.normalCore_normal
exact le_antisymm (relIndex_eq_one.mp this) (normalCore_le H)
have : Finite G := finite_of_card_ne_zero hG0
have index_ne_zero : H.index ≠ 0 := index_ne_zero_of_finite
rw [← mul_left_inj' index_ne_zero, one_mul, relIndex_mul_index H.normalCore_le]
have hp : Nat.Prime H.index := hHp ▸ minFac_prime hG1
have h : H.normalCore.index ∣ H.index ! :=
by
rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]
exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range
apply dvd_antisymm _ (index_dvd_of_le H.normalCore_le)
rwa [← Coprime.dvd_mul_right, mul_factorial_pred hp.ne_zero]
have hr1 : H.normalCore.index ≠ 1 := fun hr1 ↦
hp.ne_one <| Nat.eq_one_of_dvd_one (hr1 ▸ H.normalCore.index_dvd_of_le H.normalCore_le)
rw [Nat.coprime_factorial_iff hr1]
exact
lt_of_lt_of_le (Nat.sub_one_lt hp.ne_zero) <|
hHp ▸
minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
(dvd_trans (minFac_dvd H.normalCore.index) (H.normalCore.index_dvd_card))
