English
If p is prime and p ∤ n, then expand R p (cyclotomic n R) equals cyclotomic (n p) R multiplied by cyclotomic n R.
Русский
Если p — простое и p не делит n, то expand R p (cyclotomic n R) = cyclotomic (n p) R · cyclotomic n R.
LaTeX
$$expand R p (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R$$
Lean4
/-- If `p` is a prime such that `p ∣ n`, then
`expand R p (cyclotomic n R) = cyclotomic (p * n) R`. -/
@[simp]
theorem cyclotomic_expand_eq_cyclotomic {p n : ℕ} (hp : Nat.Prime p) (hdiv : p ∣ n) (R : Type*) [CommRing R] :
expand R p (cyclotomic n R) = cyclotomic (n * p) R :=
by
rcases n.eq_zero_or_pos with (rfl | hzero)
· simp
haveI := NeZero.of_pos hzero
suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by
rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]
refine eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ ℤ) ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_
· have hpos := Nat.mul_pos hzero hp.pos
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm
rw [cyclotomic_eq_minpoly hprim hpos]
refine minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) ?_
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 _ hp.pos]
·
rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]
