Documentation

Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Unique factorization #

Main Definitions #

@[reducible, inline]
abbrev WfDvdMonoid (α : Type u_2) [CommMonoidWithZero α] :

Well-foundedness of the strict version of ∣, which is equivalent to the descending chain condition on divisibility and to the ascending chain condition on principal ideals in an integral domain.

Equations
theorem WfDvdMonoid.exists_irreducible_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a : α} (ha : ¬IsUnit a) (ha0 : a 0) :
∃ (i : α), Irreducible i i a
theorem WfDvdMonoid.induction_on_irreducible {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {P : αProp} (a : α) (h0 : P 0) (hu : ∀ (u : α), IsUnit uP u) (hi : ∀ (a i : α), a 0Irreducible iP aP (i * a)) :
P a
theorem WfDvdMonoid.exists_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) :
a 0∃ (f : Multiset α), (∀ bf, Irreducible b) Associated f.prod a
theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) (hn0 : a 0) :
¬IsUnit a ∃ (f : Multiset α), (∀ bf, Irreducible b) f.prod = a f
theorem WfDvdMonoid.isRelPrime_of_no_irreducible_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {x y : α} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : α), Irreducible zz x¬z y) :

unique factorization monoids.

These are defined as CancelCommMonoidWithZeros 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

Instances
    theorem UniqueFactorizationMonoid.exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :
    a 0∃ (f : Multiset α), (∀ bf, Prime b) Associated f.prod a
    theorem UniqueFactorizationMonoid.induction_on_prime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : αProp} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), IsUnit xP x) (h₃ : ∀ (a p : α), a 0Prime pP aP (p * a)) :
    P a

    Noncomputably determines the multiset of prime factors.

    Equations