Description: A monic polynomial is a polynomial. (Contributed by Stefan O'Rear, 5-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | mncply | ⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑃 ∈ ( Poly ‘ 𝑆 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmnc | ⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) ↔ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = 1 ) ) | |
2 | 1 | simplbi | ⊢ ( 𝑃 ∈ ( Monic ‘ 𝑆 ) → 𝑃 ∈ ( Poly ‘ 𝑆 ) ) |