Metamath Proof Explorer


Theorem mnccoe

Description: A monic polynomial has leading coefficient 1. (Contributed by Stefan O'Rear, 5-Dec-2014)

Ref Expression
Assertion mnccoe P Monic S coeff P deg P = 1

Proof

Step Hyp Ref Expression
1 elmnc P Monic S P Poly S coeff P deg P = 1
2 1 simprbi P Monic S coeff P deg P = 1