Theorem: AdjoinRoot.aeval_root (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p : ℕ
hpri : Fact p.Prime
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ (aeval (root P)) P = 0
Tactic:
simp
State after:
no goals