English
The reduction modulo p of the minimal polynomial of μ is separable when p is prime and p ∤ n.
Русский
Редукция по модулю p минимального многочлена μ сепарабельна, когда p — простое число и p не делит n.
LaTeX
$$separable_minpoly_mod {p} [Fact p.Prime] (hdiv : ¬p ∣ n) : Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))$$
Lean4
/-- The reduction modulo `p` of the minimal polynomial of a root of unity `μ` is separable. -/
theorem separable_minpoly_mod {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) :
Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)) :=
by
have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 :=
by
convert _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]
refine Separable.of_dvd (separable_X_pow_sub_C 1 ?_ one_ne_zero) hdvd
by_contra hzero
exact hdiv ((ZMod.natCast_eq_zero_iff n p).1 hzero)
