theorem :: FIELD_15:20

for R being domRing
for p being Polynomial of R
for n being Nat holds LC (p `^ n) = (LC p) |^ n