Finiteness of divisors

Main results

• UniqueFactorizationMonoid.fintypeSubtypeDvd: elements of a UFM with finitely many units have finitely many divisors.

@[implicit_reducible]

noncomputable def UniqueFactorizationMonoid.fintypeSubtypeDvd {M : Type u_2} [CommMonoidWithZero M] [UniqueFactorizationMonoid M] [Fintype Mˣ] (y : M) (hy : y ≠ 0) : Fintype { x : M // x ∣ y }

If y is a nonzero element of a unique factorization monoid with finitely many units (e.g. ℤ, Ideal (ring_of_integers K)), it has finitely many divisors.