theorem exevalLM: :: FIELD_6:29

for R being non degenerated Ring
for S being RingExtension of R
for a, b being Element of S
for p being non zero Polynomial of R st b = LC p holds
Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p))