# Finiteness of divisors #

## Main results #

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

source
noncomputable def UniqueFactorizationMonoid.fintypeSubtypeDvd {M : Type u_2} [CancelCommMonoidWithZero 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.

Equations

- One or more equations did not get rendered due to their size.

Instances For