Division of univariate polynomials #
The main defs are divByMonic
and modByMonic
.
The compatibility between these is given by modByMonic_add_div
.
We also define rootMultiplicity
.
See divByMonic
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
divByMonic
gives the quotient of p
by a monic polynomial q
.
Instances For
modByMonic
gives the remainder of p
by a monic polynomial q
.
Instances For
divByMonic
gives the quotient of p
by a monic polynomial q
.
Equations
- Polynomial.«term_/ₘ_» = Lean.ParserDescr.trailingNode `Polynomial.term_/ₘ_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /ₘ ") (Lean.ParserDescr.cat `term 71))
Instances For
modByMonic
gives the remainder of p
by a monic polynomial q
.
Equations
- Polynomial.«term_%ₘ_» = Lean.ParserDescr.trailingNode `Polynomial.term_%ₘ_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " %ₘ ") (Lean.ParserDescr.cat `term 71))
Instances For
Alias of Polynomial.modByMonic_eq_zero_iff_dvd
.
See Polynomial.mul_left_modByMonic
for the other multiplication order. That version, unlike
this one, requires commutativity.
Alias of Polynomial.mul_divByMonic_cancel_left
.
An algorithm for deciding polynomial divisibility.
The algorithm is "compute p %ₘ q
and compare to 0
".
See polynomial.modByMonic
for the algorithm that computes %ₘ
.
Equations
- Polynomial.decidableDvdMonic p hq = decidable_of_iff (p %ₘ q = 0) ⋯
Instances For
The largest power of X - C a
which divides p
.
This could be computable via the divisibility algorithm Polynomial.decidableDvdMonic
,
as shown by Polynomial.rootMultiplicity_eq_nat_find_of_nonzero
which has a computable RHS.
Equations
- One or more equations did not get rendered due to their size.
Instances For
See Polynomial.mul_right_modByMonic
for the other multiplication order. This version, unlike
that one, requires commutativity.