Theorems · Definition · commutative algebra

Polynomial.fintypeSubtypeMonicDvd

{D : Type u} →
  [inst : CommRing D] → [UniqueFactorizationMonoid D] → (f : Polynomial D) → f ≠ 0 → Fintype { g // 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.

Defined in

Mathlib.RingTheory.Polynomial.UniqueFactorization

Cited by

0 results in Mathlib

Foundations

Depth 120 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingUniqueFactorizationMonoid