Theory of univariate polynomials #
This file starts looking like the ring theory of $R[X]$
Equations
- One or more equations did not get rendered due to their size.
Division of polynomials. See Polynomial.divByMonic
for more details.
Instances For
Remainder of polynomial division. See Polynomial.modByMonic
for more details.
Instances For
Equations
- Polynomial.instDiv = { div := Polynomial.div }
Equations
- Polynomial.instMod = { mod := Polynomial.mod }
Equations
- Polynomial.instEuclideanDomain = EuclideanDomain.mk (fun (x1 x2 : Polynomial R) => x1 / x2) ⋯ (fun (x1 x2 : Polynomial R) => x1 % x2) ⋯ (fun (p q : Polynomial R) => p.degree < q.degree) ⋯ ⋯ ⋯
If f
is a polynomial over a field, and a : K
satisfies f' a ≠ 0
,
then f / (X - a)
is coprime with X - a
.
Note that we do not assume f a = 0
, because f / (X - a) = (f - f a) / (X - a)
.
To check a polynomial over a field is irreducible, it suffices to check only for divisors that have smaller degree.
See also: Polynomial.Monic.irreducible_iff_natDegree
.
To check a polynomial p
over a field is irreducible, it suffices to check there are no
divisors of degree 0 < d ≤ degree p / 2
.
See also: Polynomial.Monic.irreducible_iff_natDegree'
.
An irreducible polynomial over a field must have positive degree.