apply Polynomial.map_injective (algebraMap ℤ ℚ) (RingHom.injective_int (algebraMap ℤ ℚ))
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ minpoly ℤ x = cyclotomic p ℤ
case a
p : ℕ
hpri : Fact p.Prime
x : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hx : IsPrimitiveRoot (↑x) p
⊢ map (algebraMap ℤ ℚ) (minpoly ℤ x) = map (algebraMap ℤ ℚ) (cyclotomic p ℤ)