English
If m is coprime to n, the minimal polynomials of μ and μ^m are equal.
Русский
Если m взаимно простое с n, то минимальные полиномы μ и μ^m совпадают.
LaTeX
$$$\minpoly_{\mathbb{Z}}(\mu) = \minpoly_{\mathbb{Z}}(\mu^{m})$ при $\gcd(m,n)=1$$$
Lean4
/-- If `m : ℕ` is coprime with `n`,
then the minimal polynomials of a primitive `n`-th root of unity `μ`
and of `μ ^ m` are the same. -/
theorem minpoly_eq_pow_coprime {m : ℕ} (hcop : Nat.Coprime m n) : minpoly ℤ μ = minpoly ℤ (μ ^ m) :=
by
revert n hcop
refine UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_
· intro h hn
congr
simpa [(Nat.coprime_zero_left _).mp hn] using h
· intro u hunit _ _
congr
simp [Nat.isUnit_iff.mp hunit]
· intro a p _ hprime hind h hcop
rw [hind h (Nat.Coprime.coprime_mul_left hcop)]; clear hind
replace hprime := hprime.nat_prime
have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)
haveI := Fact.mk hprime
rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.Coprime.coprime_mul_left hcop)) hdiv]
congr 1
ring
