Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Stefan O'Rear
Additional material on polynomials [DEPRECATED]
df-mnc
Next ⟩
df-plylt
Metamath Proof Explorer
Ascii
Unicode
Definition
df-mnc
Description:
Define the class of monic polynomials.
(Contributed by
Stefan O'Rear
, 5-Dec-2014)
Ref
Expression
Assertion
df-mnc
⊢
Monic
=
s
∈
𝒫
ℂ
⟼
p
∈
Poly
⁡
s
|
coeff
⁡
p
⁡
deg
⁡
p
=
1
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cmnc
class
Monic
1
vs
setvar
s
2
cc
class
ℂ
3
2
cpw
class
𝒫
ℂ
4
vp
setvar
p
5
cply
class
Poly
6
1
cv
setvar
s
7
6
5
cfv
class
Poly
⁡
s
8
ccoe
class
coeff
9
4
cv
setvar
p
10
9
8
cfv
class
coeff
⁡
p
11
cdgr
class
deg
12
9
11
cfv
class
deg
⁡
p
13
12
10
cfv
class
coeff
⁡
p
⁡
deg
⁡
p
14
c1
class
1
15
13
14
wceq
wff
coeff
⁡
p
⁡
deg
⁡
p
=
1
16
15
4
7
crab
class
p
∈
Poly
⁡
s
|
coeff
⁡
p
⁡
deg
⁡
p
=
1
17
1
3
16
cmpt
class
s
∈
𝒫
ℂ
⟼
p
∈
Poly
⁡
s
|
coeff
⁡
p
⁡
deg
⁡
p
=
1
18
0
17
wceq
wff
Monic
=
s
∈
𝒫
ℂ
⟼
p
∈
Poly
⁡
s
|
coeff
⁡
p
⁡
deg
⁡
p
=
1