let F be Field; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds
( p is monic iff NormPolynomial p = p )
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( p is monic iff NormPolynomial p = p )
hereby :: thesis: ( NormPolynomial p = p implies p is monic )
assume p is monic ; :: thesis: NormPolynomial p = p
then LC p = 1. F by RATFUNC1:def 7;
hence NormPolynomial p = ((1. F) ") * p by npl
.= p by poly2a ;
:: thesis: verum
end;
thus ( NormPolynomial p = p implies p is monic ) ; :: thesis: verum