Nuprl Definition : polyform-lead-nonzero
polyform-lead-nonzero(n;p) == 0 < n ⇒ 0 < ||p|| ⇒ (¬↑poly-zero(n - 1;hd(p)))
Definitions occuring in Statement :
poly-zero: poly-zero(n;p),
hd: hd(l),
length: ||as||,
assert: ↑b,
less_than: a < b,
not: ¬A,
implies: P ⇒ Q,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
implies: P ⇒ Q,
less_than: a < b,
length: ||as||,
not: ¬A,
assert: ↑b,
poly-zero: poly-zero(n;p),
subtract: n - m,
natural_number: $n,
hd: hd(l)
FDL editor aliases :
polyform-lead-nonzero
Latex:
polyform-lead-nonzero(n;p) == 0 < n {}\mRightarrow{} 0 < ||p|| {}\mRightarrow{} (\mneg{}\muparrow{}poly-zero(n - 1;hd(p)))
Date html generated:
2017_09_29-PM-05_59_46
Last ObjectModification:
2017_04_26-PM-02_04_25
Theory : integer!polynomials
Home
Index