English
In characteristic p, with p ∤ m, a element μ is a root of cyclotomic(p^k · m) over R if and only if μ is a primitive m-th root of unity.
Русский
При характеристике p и p не делит m, элемент μ является корнем cyclotomic(p^k · m) над R тогда и только тогда, когда μ является примитивным m-ым корнем единицы.
LaTeX
$$$$ (\\operatorname{cyclotomic}(p^k \\cdot m, R)).\\text{IsRoot}(\\mu) \\;\\Longleftrightarrow\\; \\text{IsPrimitiveRoot}(\\mu, m). $$$$
Lean4
/-- If `R` is of characteristic `p` and `¬p ∣ m`, then `ζ` is a root of `cyclotomic (p ^ k * m) R`
if and only if it is a primitive `m`-th root of unity. -/
theorem isRoot_cyclotomic_prime_pow_mul_iff_of_charP {m k p : ℕ} {R : Type*} [CommRing R] [IsDomain R]
[hp : Fact (Nat.Prime p)] [hchar : CharP R p] {μ : R} [NeZero (m : R)] :
(Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m :=
by
rcases k.eq_zero_or_pos with (rfl | hk)
· rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
refine ⟨fun h => ?_, fun h => ?_⟩
· rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow] at h
replace h := pow_eq_zero h
rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h
· rw [← isRoot_cyclotomic_iff, IsRoot.def] at h
rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow, h, zero_pow]
exact Nat.sub_ne_zero_of_lt <| pow_right_strictMono₀ hp.out.one_lt <| Nat.pred_lt hk.ne'
