let R be non degenerated Ring; :: thesis: 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))
let S be RingExtension of R; :: thesis: 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))
let a, b be Element of S; :: thesis: for p being non zero Polynomial of R st b = LC p holds
Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p))
let p be non zero Polynomial of R; :: thesis: ( b = LC p implies Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p)) )
assume AS: b = LC p ; :: thesis: Ext_eval ((Leading-Monomial p),a) = b * (a |^ (deg p))
H0: R is Subring of S by FIELD_4:def 1;
H2: p . ((len p) -' 1) = LC p by RATFUNC1:def 6;
deg p = (len p) - 1 by HURWITZ:def 2;
then H3: (len p) -' 1 = deg p by XREAL_0:def 2;
thus Ext_eval ((Leading-Monomial p),a) = (In ((p . ((len p) -' 1)),S)) * ((power S) . (a,((len p) -' 1))) by H0, ALGNUM_1:17
.= b * (a |^ (deg p)) by AS, H2, H3, BINOM:def 2 ; :: thesis: verum