Theorems · Definition · commutative algebra

Associates.FactorSet

(α : Type u) → [CommMonoidWithZero α] → Type u

FactorSet α representation elements of unique factorization domain as multisets. Multiset α produced by normalizedFactors are only unique up to associated elements, while the multisets in FactorSet α are unique by equality and restricted to irreducible elements. This gives us a representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete lattice structure. Infimum is the greatest common divisor and supremum is the least common multiple.

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Cited by

52 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CommMonoidWithZero