English
The primitive roots of order n in K are contained among the roots of the minimal polynomial of a primitive n-th root μ, after mapping coefficients to K.
Русский
Примитивные корни степени n в K включаются в корни минимального полинома примитивного μ степени n после замены коэффициентов на элементы кольца K.
LaTeX
$$$\mathrm{primitiveRoots}(n,K) \subseteq \mathrm{roots}\left(\operatorname{map}(\operatorname{Int.castRingHom} K)(\minpoly_{\mathbb{Z}}(\mu))\right)$$
Lean4
/-- `primitiveRoots n K` is a subset of the roots of the minimal polynomial of a primitive
`n`-th root of unity `μ`. -/
theorem is_roots_of_minpoly [DecidableEq K] :
primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset :=
by
by_cases hn : n = 0; · simp_all
have : NeZero n := ⟨hn⟩
have hpos := Nat.pos_of_ne_zero hn
intro x hx
obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h).1 ((mem_primitiveRoots hpos).1 hx)
simp only [Multiset.mem_toFinset]
convert pow_isRoot_minpoly h hcop using 0
rw [← mem_roots]
exact map_monic_ne_zero <| minpoly.monic <| isIntegral h hpos
