# Basic results un unique factorization monoids #

## Main results #

- `prime_factors_unique`: the prime factors of an element in a cancellative commutative monoid with zero (e.g. an integral domain) are unique up to associates
- `UniqueFactorizationMonoid.factors_unique`: the irreducible factors of an element in a unique factorization monoid (e.g. a UFD) are unique up to associates
- `UniqueFactorizationMonoid.iff_exists_prime_factors`: unique factorization exists iff each nonzero elements factors into a product of primes
- `UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors`: Euclid's lemma: if `a ∣ b * c` and `a` and `c` have no common prime factors, `a ∣ b`.
- `UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors`: Euclid's lemma: if `a ∣ b * c` and `a` and `b` have no common prime factors, `a ∣ c`.
- `UniqueFactorizationMonoid.exists_reduced_factors`: in a UFM, we can divide out a common factor to get relatively prime elements.

source
theorem WfDvdMonoid.of_wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] :
WfDvdMonoid (Associates α) → WfDvdMonoid α
source
instance WfDvdMonoid.wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] :
WfDvdMonoid (Associates α)
source
theorem WfDvdMonoid.wellFoundedLT_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] :
WellFoundedLT (Associates α)
source
theorem WfDvdMonoid.of_wellFoundedLT_associates {α : Type u_1} [CancelCommMonoidWithZero α] (h : WellFoundedLT (Associates α)) :
WfDvdMonoid α
source
theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] :
WfDvdMonoid α ↔ WellFoundedLT (Associates α)
source
instance Associates.ufm {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :
UniqueFactorizationMonoid (Associates α)
source
theorem prime_factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] {f g : Multiset α} :
(∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → Associated f.prod g.prod → Multiset.Rel Associated f g
source
theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g
source
theorem prime_factors_irreducible {α : Type u_1} [CommMonoidWithZero α] {a : α} {f : Multiset α} (ha : Irreducible a) (pfa : (∀ b ∈ f, Prime b) ∧ Associated f.prod a) :
∃ (p : α), Associated a p ∧ f = {p}

If an irreducible has a prime factorization, then it is an associate of one of its prime factors.

source
theorem irreducible_iff_prime_of_existsUnique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) (p : α) :
Irreducible p ↔ Prime p
source
@[simp]
theorem UniqueFactorizationMonoid.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :
factors 1 = 0
source
theorem UniqueFactorizationMonoid.exists_mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
p ∣ a → ∃ q ∈ factors a, Associated p q
source
theorem UniqueFactorizationMonoid.exists_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :
∃ (p : α), p ∈ factors x
source
theorem UniqueFactorizationMonoid.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
Multiset.Rel Associated (factors (x * y)) (factors x + factors y)
source
theorem UniqueFactorizationMonoid.factors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) :
Multiset.Rel Associated (factors (x ^ n)) (n • factors x)
source
@[simp]
theorem UniqueFactorizationMonoid.factors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) :
0 < factors x ↔ ¬IsUnit x
source
theorem UniqueFactorizationMonoid.factors_pow_count_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {x : α} (hx : x ≠ 0) :
Associated (∏ p ∈ (factors x).toFinset, p ^ Multiset.count p (factors x)) x
source
theorem UniqueFactorizationMonoid.factors_rel_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) :
Multiset.Rel Associated (factors a) (factors b)
source
theorem Associates.unique' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p q : Multiset (Associates α)} :
(∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q
source
theorem Associates.prod_le_prod_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p q : Multiset (Associates α)} (hp : ∀ a ∈ p, Irreducible a) (hq : ∀ a ∈ q, Irreducible a) :
p.prod ≤ q.prod ↔ p ≤ q
source
theorem WfDvdMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) :
WfDvdMonoid α
source
theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) {p : α} :
Irreducible p ↔ Prime p
source
theorem UniqueFactorizationMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) :
UniqueFactorizationMonoid α
source
theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] :
UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
source
theorem MulEquiv.uniqueFactorizationMonoid {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [CancelCommMonoidWithZero β] (e : α ≃* β) (hα : UniqueFactorizationMonoid α) :
UniqueFactorizationMonoid β
source
theorem MulEquiv.uniqueFactorizationMonoid_iff {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [CancelCommMonoidWithZero β] (e : α ≃* β) :
UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β
source
theorem UniqueFactorizationMonoid.of_existsUnique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) :
UniqueFactorizationMonoid α
source
theorem UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) :
IsRelPrime a b ↔ ∀ ⦃d : R⦄, d ∣ a → d ∣ b → ¬Prime d
source
theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b c : R} (ha : a ≠ 0) (h : ∀ ⦃d : R⦄, d ∣ a → d ∣ c → ¬Prime d) :
a ∣ b * c → a ∣ b

Euclid's lemma: if `a ∣ b * c` and `a` and `c` have no common prime factors, `a ∣ b`. Compare `IsCoprime.dvd_of_dvd_mul_left`.

source
theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b c : R} (ha : a ≠ 0) (no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) :
a ∣ b * c → a ∣ c

Euclid's lemma: if `a ∣ b * c` and `a` and `b` have no common prime factors, `a ∣ c`. Compare `IsCoprime.dvd_of_dvd_mul_right`.

source
theorem UniqueFactorizationMonoid.exists_reduced_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R) :
a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

If `a ≠ 0, b` are elements of a unique factorization domain, then dividing out their common factor `c'` gives `a'` and `b'` with no factors in common.

source
theorem UniqueFactorizationMonoid.exists_reduced_factors' {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] (a b : R) (hb : b ≠ 0) :
∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b