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.

theorem WfDvdMonoid.of_wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] : WfDvdMonoid (Associates α) → WfDvdMonoid α

instance WfDvdMonoid.wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] : WfDvdMonoid (Associates α)

theorem WfDvdMonoid.wellFoundedLT_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] : WellFoundedLT (Associates α)

@[deprecated WfDvdMonoid.wellFoundedLT_associates (since := "2024-09-02")]

theorem WfDvdMonoid.wellFounded_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] : WellFounded fun (x1 x2 : Associates α) => x1 < x2

theorem WfDvdMonoid.of_wellFoundedLT_associates {α : Type u_1} [CancelCommMonoidWithZero α] (h : WellFoundedLT (Associates α)) : WfDvdMonoid α

@[deprecated WfDvdMonoid.of_wellFoundedLT_associates (since := "2024-09-02")]

theorem WfDvdMonoid.of_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] (h : WellFounded fun (x1 x2 : Associates α) => x1 < x2) : WfDvdMonoid α

theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] : WfDvdMonoid α ↔ WellFoundedLT (Associates α)

instance Associates.ufm {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid (Associates α)

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

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

theorem prime_factors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] {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.

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

@[deprecated irreducible_iff_prime_of_existsUnique_irreducible_factors (since := "2024-12-17")]

theorem irreducible_iff_prime_of_exists_unique_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

Alias of irreducible_iff_prime_of_existsUnique_irreducible_factors.

@[simp]

theorem UniqueFactorizationMonoid.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : factors 1 = 0

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

theorem UniqueFactorizationMonoid.exists_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ (p : α), p ∈ factors x

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)

theorem UniqueFactorizationMonoid.factors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) : Multiset.Rel Associated (factors (x ^ n)) (n • factors x)

@[simp]

theorem UniqueFactorizationMonoid.factors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) : 0 < factors x ↔ ¬IsUnit x

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

theorem UniqueFactorizationMonoid.factors_rel_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : Multiset.Rel Associated (factors a) (factors b)

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

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

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 α

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

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 α

theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] : UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a

theorem MulEquiv.uniqueFactorizationMonoid {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [CancelCommMonoidWithZero β] (e : α ≃* β) (hα : UniqueFactorizationMonoid α) : UniqueFactorizationMonoid β

theorem MulEquiv.uniqueFactorizationMonoid_iff {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [CancelCommMonoidWithZero β] (e : α ≃* β) : UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β

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 α

@[deprecated UniqueFactorizationMonoid.of_existsUnique_irreducible_factors (since := "2024-12-17")]

theorem UniqueFactorizationMonoid.of_exists_unique_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 α

Alias of UniqueFactorizationMonoid.of_existsUnique_irreducible_factors.

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

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.

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.

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.

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

@[deprecated pow_injective_of_not_isUnit (since := "2024-09-21")]

theorem UniqueFactorizationMonoid.pow_right_injective {M : Type u_1} [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) : Function.Injective fun (n : ℕ) => q ^ n

Alias of pow_injective_of_not_isUnit.

@[deprecated pow_inj_of_not_isUnit (since := "2024-09-21")]

theorem UniqueFactorizationMonoid.pow_eq_pow_iff {M : Type u_1} [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) {m n : ℕ} : q ^ m = q ^ n ↔ m = n

Alias of pow_inj_of_not_isUnit.