Theorems · Definition · commutative algebra

UniqueFactorizationMonoid.fintypeSubtypeDvd

{M : Type u_2} →
  [inst : CommMonoidWithZero M] →
    [UniqueFactorizationMonoid M] → [Fintype Mˣ] → (y : M) → y ≠ 0 → Fintype { x // 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.

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroUniqueFactorizationMonoidFintype