Structures · Algebra

UniqueFactorizationMonoid

Unique factorization monoids are defined as cancellative CommMonoidWithZeros with well-founded strict divisibility relations, but this is equivalent to more familiar definitions: Each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements. Each element (except zero) is non-uniquely represented as a multiset of prime factors. To define a UFD using the definition in terms of multisets of irreducible factors, use the definition of_existsUnique_irreducible_factors To define a UFD using the definition in terms of multisets of prime factors, use the definition of_exists_prime_factors

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Shape

One type argument · adds irreducible_iff_prime