Documentation

Mathlib.RingTheory.Polynomial.UniqueFactorization

Unique factorization for univariate and multivariate polynomials #

Main results #

@[instance 100]

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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