Unique factorization for univariate and multivariate polynomials

Main results

• Polynomial.wfDvdMonoid: If an integral domain is a WFDvdMonoid, then so is its polynomial ring.
• Polynomial.uniqueFactorizationMonoid, MvPolynomial.uniqueFactorizationMonoid: If an integral domain is a UniqueFactorizationMonoid, then so is its polynomial ring (of any number of variables).

@[instance 100]

instance Polynomial.wfDvdMonoid {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] : WfDvdMonoid (Polynomial R)

theorem Polynomial.exists_irreducible_of_degree_pos {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] {f : Polynomial R} [Nontrivial R] (hf : 0 < f.degree) : ∃ (g : Polynomial R), Irreducible g ∧ g ∣ f

theorem Polynomial.exists_irreducible_of_natDegree_pos {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] {f : Polynomial R} [Nontrivial R] (hf : 0 < f.natDegree) : ∃ (g : Polynomial R), Irreducible g ∧ g ∣ f

theorem Polynomial.exists_irreducible_of_natDegree_ne_zero {R : Type u_1} [CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] {f : Polynomial R} [Nontrivial R] (hf : f.natDegree ≠ 0) : ∃ (g : Polynomial R), Irreducible g ∧ g ∣ f

@[instance 100]

instance Polynomial.uniqueFactorizationMonoid {D : Type u} [CommRing D] [UniqueFactorizationMonoid D] : UniqueFactorizationMonoid (Polynomial D)

@[instance_reducible]

noncomputable def Polynomial.fintypeSubtypeMonicDvd {D : Type u} [CommRing D] [UniqueFactorizationMonoid D] (f : Polynomial D) (hf : f ≠ 0) : Fintype { g : Polynomial D // g.Monic ∧ g ∣ f }

If D is a unique factorization domain, f is a non-zero polynomial in D[X], then f has only finitely many monic factors. (Note that its factors up to unit may be more than monic factors.) See also UniqueFactorizationMonoid.fintypeSubtypeDvd.

@[instance 100]

instance MvPolynomial.uniqueFactorizationMonoid (σ : Type v) {D : Type u} [CommRing D] [UniqueFactorizationMonoid D] : UniqueFactorizationMonoid (MvPolynomial σ D)

theorem Polynomial.exists_monic_irreducible_factor {F : Type u_1} [Field F] (f : Polynomial F) (hu : ¬IsUnit f) : ∃ (g : Polynomial F), g.Monic ∧ Irreducible g ∧ g ∣ f

A polynomial over a field which is not a unit must have a monic irreducible factor. See also WfDvdMonoid.exists_irreducible_factor.