Documentation

Mathlib.Algebra.Polynomial.RingDivision

Theory of univariate polynomials #

We prove basic results about univariate polynomials.

theorem Polynomial.natDegree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p 0) {z : S} (hz : (aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0x = 0) :
theorem Polynomial.degree_pos_of_aeval_root {R : Type u} {S : Type v} [CommRing R] [Semiring S] [Algebra R S] {p : Polynomial R} (hp : p 0) {z : S} (hz : (aeval z) p = 0) (inj : ∀ (x : R), (algebraMap R S) x = 0x = 0) :
theorem Polynomial.smul_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (c : R) (p : Polynomial R) :

_ %ₘ q as an R-linear map.

Equations
Instances For
    theorem Polynomial.aeval_modByMonic_eq_self_of_root {R : Type u} {S : Type v} [CommRing R] [Ring S] [Algebra R S] {p q : Polynomial R} (hq : q.Monic) {x : S} (hx : (aeval x) q = 0) :
    (aeval x) (p %ₘ q) = (aeval x) p
    theorem Polynomial.rootMultiplicity_X_sub_C_pow {R : Type u} [CommRing R] [Nontrivial R] (a : R) (n : ) :

    The multiplicity of a as root of (X - a) ^ n is n.

    theorem Polynomial.prime_X_sub_C {R : Type u} [CommRing R] [IsDomain R] (r : R) :
    Prime (X - C r)
    theorem Polynomial.aeval_ne_zero_of_isCoprime {S : Type v} {R : Type u_1} [CommSemiring R] [Nontrivial S] [Semiring S] [Algebra R S] {p q : Polynomial R} (h : IsCoprime p q) (s : S) :
    (aeval s) p 0 (aeval s) q 0
    theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (a - b)) :
    IsCoprime (X - C a) (X - C b)
    theorem Polynomial.pairwise_coprime_X_sub_C {K : Type u_1} [Field K] {I : Type v} {s : IK} (H : Function.Injective s) :
    Pairwise (Function.onFun IsCoprime fun (i : I) => X - C (s i))
    @[irreducible]
    theorem Polynomial.exists_multiset_roots {R : Type u} [CommRing R] [IsDomain R] [DecidableEq R] {p : Polynomial R} :
    p 0∃ (s : Multiset R), s.card p.degree ∀ (a : R), Multiset.count a s = rootMultiplicity a p