let R be domRing; :: thesis: for p being non constant Polynomial of R holds LM p = ((p . (deg p)) * (anpoly ((1. R),((deg p) -' 1)))) *' (anpoly ((1. R),1))
let p be non constant Polynomial of R; :: thesis: LM p = ((p . (deg p)) * (anpoly ((1. R),((deg p) -' 1)))) *' (anpoly ((1. R),1))
A1: not p is constant ;
then A2: deg p >= 0 + 1 by INT_1:7;
reconsider n = (deg p) - 1 as Nat by A1;
len p = (deg p) + 1 ;
then not p . (deg p) is zero by ALGSEQ_1:10;
then reconsider a = p . (deg p) as non zero Element of R ;
A4: anpoly (a,n) = anpoly (((1. R) * a),n)
.= a * (anpoly ((1. R),n)) by FIELD_1:9 ;
LM p = anpoly ((a * (1. R)),(n + 1)) by FIELD_1:11
.= (a * (anpoly ((1. R),n))) *' (anpoly ((1. R),1)) by A4, FIELD_1:10
.= ((p . (deg p)) * (anpoly ((1. R),((deg p) -' 1)))) *' (anpoly ((1. R),1)) by A2, XREAL_1:233 ;
hence LM p = ((p . (deg p)) * (anpoly ((1. R),((deg p) -' 1)))) *' (anpoly ((1. R),1)) ; :: thesis: verum