English
If the cyclotomic polynomial of p^n is irreducible, so is the cyclotomic of p^m for m ≤ n.
Русский
Если цикілотромический многочлен p^n ирредуцируем, то и p^m ирредуцируем при m ≤ n.
LaTeX
$$Irreducible( cyclotomic(p^m, R) ) given Irreducible( cyclotomic(p^n, R) ) and m ≤ n$$
Lean4
/-- If `p` is a prime such that `¬ p ∣ n`, then
`expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R)`. -/
@[simp]
theorem cyclotomic_expand_eq_cyclotomic_mul {p n : ℕ} (hp : Nat.Prime p) (hdiv : ¬p ∣ n) (R : Type*) [CommRing R] :
expand R p (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R :=
by
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
· simp
haveI := NeZero.of_pos hnpos
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ by
rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic]
refine
eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ ℤ))
((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_
· refine
(IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast _ _
(IsPrimitive.mul (cyclotomic.isPrimitive (n * p) ℤ) (cyclotomic.isPrimitive n ℤ))
((cyclotomic.monic n ℤ).expand hp.pos).isPrimitive).2
?_
rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int]
refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_
· replace h : n * p = n * 1 := by simp [h]
exact Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)
· have hpos : 0 < n * p := mul_pos hnpos hp.pos
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
rw [cyclotomic_eq_minpoly_rat hprim hpos]
refine minpoly.dvd ℚ _ ?_
rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, @isRoot_cyclotomic_iff]
convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
· have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
rw [cyclotomic_eq_minpoly_rat hprim hnpos]
refine minpoly.dvd ℚ _ ?_
rw [aeval_def, ← eval_map, map_expand, expand_eval, ← IsRoot.def, ← cyclotomic_eq_minpoly_rat hprim hnpos,
map_cyclotomic, @isRoot_cyclotomic_iff]
exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv
·
rw [natDegree_expand, natDegree_cyclotomic, natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ),
natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv), Nat.totient_prime hp, mul_comm (p - 1), ←
Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]
