English
Assume σ is a type, D a UFD, then the polynomial ring D[X] is a UFD; every nonzero polynomial has a finite irreducible decomposition.
Русский
Пусть D — UFD, тогда D[X] — тоже UFD; любой ненулевой полином имеет конечное разложение на иррекобилизируемые множители.
LaTeX
$$$$\\text{In particular } D[X] \\text{ is a UFD whenever } D \\text{ is a UFD}. $$$$
Lean4
/-- 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`. -/
noncomputable def fintypeSubtypeMonicDvd (f : D[X]) (hf : f ≠ 0) : Fintype { g : D[X] // g.Monic ∧ g ∣ f } :=
by
set G := { g : D[X] // g.Monic ∧ g ∣ f }
let y : Associates D[X] := Associates.mk f
have hy : y ≠ 0 := Associates.mk_ne_zero.mpr hf
let H := { x : Associates D[X] // x ∣ y }
let hfin : Fintype H := UniqueFactorizationMonoid.fintypeSubtypeDvd y hy
let i : G → H := fun x ↦ ⟨Associates.mk x.1, Associates.mk_dvd_mk.2 x.2.2⟩
refine Fintype.ofInjective i fun x y heq ↦ ?_
rw [Subtype.mk.injEq] at heq ⊢
exact eq_of_monic_of_associated x.2.1 y.2.1 (Associates.mk_eq_mk_iff_associated.mp heq)
