Unique factorization

Main Definitions

• WfDvdMonoid holds for Monoids for which a strict divisibility relation is well-founded.
• UniqueFactorizationMonoid holds for WfDvdMonoids where Irreducible is equivalent to Prime

To do

• set up the complete lattice structure on FactorSet.

class WfDvdMonoid (α : Type u_2) [CommMonoidWithZero α] : Prop

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.

• wellFounded_dvdNotUnit : WellFounded DvdNotUnit

instance IsNoetherianRing.wfDvdMonoid {α : Type u_1} [CommRing α] [IsDomain α] [IsNoetherianRing α] : WfDvdMonoid α

Equations

• (_ : WfDvdMonoid α) = (_ : WfDvdMonoid α)

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

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

Equations

• (_ : WfDvdMonoid (Associates α)) = (_ : WfDvdMonoid (Associates α))

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

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 u → P u) (hi : ∀ (a i : α), a ≠ 0 → Irreducible i → P a → P (i * a)) : P a

theorem WfDvdMonoid.exists_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) : a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated (Multiset.prod f) a

theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) (hn0 : a ≠ 0) : ¬IsUnit a ↔ ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Multiset.prod f = a ∧ f ≠ ∅

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

theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] : WfDvdMonoid α ↔ WellFounded fun (x x_1 : Associates α) => x < x_1

class UniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends WfDvdMonoid : Prop

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_exists_unique_irreducible_factors

To define a UFD using the definition in terms of multisets of prime factors, use the definition of_exists_prime_factors

• wellFounded_dvdNotUnit : WellFounded DvdNotUnit
• irreducible_iff_prime : ∀ {a : α}, Irreducible a ↔ Prime a

@[reducible]

theorem ufm_of_gcd_of_wfDvdMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [WfDvdMonoid α] [GCDMonoid α] : UniqueFactorizationMonoid α

Can't be an instance because it would cause a loop ufm → WfDvdMonoid → ufm → ....

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

Equations

• (_ : UniqueFactorizationMonoid (Associates α)) = (_ : UniqueFactorizationMonoid (Associates α))

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

theorem UniqueFactorizationMonoid.exists_prime_iff {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x

theorem UniqueFactorizationMonoid.induction_on_prime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), IsUnit x → P x) (h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)) : P a

theorem prime_factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] {f : Multiset α} {g : Multiset α} : (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g

theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f : Multiset α} {g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated (Multiset.prod f) (Multiset.prod g)) : 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 (Multiset.prod f) 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 WfDvdMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) 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 (Multiset.prod f) 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 (Multiset.prod f) a) : UniqueFactorizationMonoid α

theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] : UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) 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 irreducible_iff_prime_of_exists_unique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated (Multiset.prod f) a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g) (p : α) : Irreducible p ↔ Prime p

theorem UniqueFactorizationMonoid.of_exists_unique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated (Multiset.prod f) a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g) : UniqueFactorizationMonoid α

noncomputable def UniqueFactorizationMonoid.factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] (a : α) : Multiset α

Noncomputably determines the multiset of prime factors.

Equations

• UniqueFactorizationMonoid.factors a = if h : a = 0 then 0 else Classical.choose (_ : ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a)

theorem UniqueFactorizationMonoid.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : Associated (Multiset.prod (UniqueFactorizationMonoid.factors a)) a

theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {p : α} {a : α} (h : p ∈ UniqueFactorizationMonoid.factors a) : a ≠ 0

theorem UniqueFactorizationMonoid.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {p : α} {a : α} (h : p ∈ UniqueFactorizationMonoid.factors a) : p ∣ a

theorem UniqueFactorizationMonoid.prime_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} (x : α) (hx : x ∈ UniqueFactorizationMonoid.factors a) : Prime x

theorem UniqueFactorizationMonoid.irreducible_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.factors a → Irreducible x

@[simp]

theorem UniqueFactorizationMonoid.factors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid.factors 0 = 0

@[simp]

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

theorem UniqueFactorizationMonoid.exists_mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.factors a, Associated p q

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

theorem UniqueFactorizationMonoid.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {x : α} {y : α} (hx : x ≠ 0) (hy : y ≠ 0) : Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x * y)) (UniqueFactorizationMonoid.factors x + UniqueFactorizationMonoid.factors y)

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

@[simp]

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

theorem UniqueFactorizationMonoid.factors_pow_count_prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) : Associated (Finset.prod (Multiset.toFinset (UniqueFactorizationMonoid.factors x)) fun (p : α) => p ^ Multiset.count p (UniqueFactorizationMonoid.factors x)) x

noncomputable def UniqueFactorizationMonoid.normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) : Multiset α

Noncomputably determines the multiset of prime factors.

Equations

• UniqueFactorizationMonoid.normalizedFactors a = Multiset.map (⇑normalize) (UniqueFactorizationMonoid.factors a)

@[simp]

theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors {M : Type u_2} [CancelCommMonoidWithZero M] [DecidableEq M] [UniqueFactorizationMonoid M] [Unique Mˣ] (x : M) : UniqueFactorizationMonoid.factors x = UniqueFactorizationMonoid.normalizedFactors x

An arbitrary choice of factors of x : M is exactly the (unique) normalized set of factors, if M has a trivial group of units.

theorem UniqueFactorizationMonoid.normalizedFactors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a

theorem UniqueFactorizationMonoid.prime_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.normalizedFactors a → Prime x

theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.normalizedFactors a → Irreducible x

theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.normalizedFactors a → normalize x = x

theorem UniqueFactorizationMonoid.normalizedFactors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) : UniqueFactorizationMonoid.normalizedFactors a = {normalize a}

theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) (p : α) : p ∈ UniqueFactorizationMonoid.normalizedFactors a → ∀ q ∈ UniqueFactorizationMonoid.normalizedFactors a, p ∣ q → p = q

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.normalizedFactors a, Associated p q

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

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid.normalizedFactors 0 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_one {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid.normalizedFactors 1 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} {y : α} (hx : x ≠ 0) (hy : y ≠ 0) : UniqueFactorizationMonoid.normalizedFactors (x * y) = UniqueFactorizationMonoid.normalizedFactors x + UniqueFactorizationMonoid.normalizedFactors y

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) : UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x

theorem Irreducible.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) : UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

theorem UniqueFactorizationMonoid.normalizedFactors_prod_eq {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) : UniqueFactorizationMonoid.normalizedFactors (Multiset.prod s) = Multiset.map (⇑normalize) s

theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} {y : α} (hx : x ≠ 0) (hy : y ≠ 0) : x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y

theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} {y : α} (hx : x ≠ 0) (hy : y ≠ 0) : Associated x y ↔ UniqueFactorizationMonoid.normalizedFactors x = UniqueFactorizationMonoid.normalizedFactors y

theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) : UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

theorem UniqueFactorizationMonoid.zero_not_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) : 0 ∉ UniqueFactorizationMonoid.normalizedFactors x

theorem UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} {p : α} (H : p ∈ UniqueFactorizationMonoid.normalizedFactors a) : p ∣ a

theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Unique αˣ] {p : α} {x : α} (hx : x ≠ 0) : p ∈ UniqueFactorizationMonoid.normalizedFactors x ↔ Prime p ∧ p ∣ x

theorem UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} {r : α} (h : ∀ {m : α}, m ∈ UniqueFactorizationMonoid.normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ (i : ℕ), Associated (p ^ i) r

theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Nontrivial α] [Unique αˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) : UniqueFactorizationMonoid.normalizedFactors (Multiset.prod m) = m

theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} {b : α} {c : α} (ha : a ∈ UniqueFactorizationMonoid.normalizedFactors c) (hb : b ∈ UniqueFactorizationMonoid.normalizedFactors c) (h : Associated a b) : a = b

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) : 0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x

theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} {y : α} (hx : x ≠ 0) (hy : y ≠ 0) : DvdNotUnit x y ↔ UniqueFactorizationMonoid.normalizedFactors x < UniqueFactorizationMonoid.normalizedFactors y

theorem UniqueFactorizationMonoid.normalizedFactors_multiset_prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : 0 ∉ s) : UniqueFactorizationMonoid.normalizedFactors (Multiset.prod s) = Multiset.sum (Multiset.map UniqueFactorizationMonoid.normalizedFactors s)

noncomputable def UniqueFactorizationMonoid.normalizationMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] [UniqueFactorizationMonoid α] : NormalizationMonoid α

Noncomputably defines a normalizationMonoid structure on a UniqueFactorizationMonoid.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance UniqueFactorizationMonoid.instInhabitedNormalizationMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] [UniqueFactorizationMonoid α] : Inhabited (NormalizationMonoid α)

Equations

• UniqueFactorizationMonoid.instInhabitedNormalizationMonoid = { default := UniqueFactorizationMonoid.normalizationMonoid }

theorem UniqueFactorizationMonoid.no_factors_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} (ha : a ≠ 0) (h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) {d : R} : d ∣ a → d ∣ b → IsUnit d

theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} {c : R} (ha : a ≠ 0) : (∀ {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 : R} {b : R} {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), (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ 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 : R) (b : R) (hb : b ≠ 0) : ∃ (a' : R) (b' : R) (c' : R), (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b

theorem UniqueFactorizationMonoid.pow_right_injective {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} (ha0 : a ≠ 0) (ha1 : ¬IsUnit a) : Function.Injective fun (x : ℕ) => a ^ x

theorem UniqueFactorizationMonoid.pow_eq_pow_iff {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} (ha0 : a ≠ 0) (ha1 : ¬IsUnit a) {i : ℕ} {j : ℕ} : a ^ i = a ^ j ↔ i = j

theorem UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [dec_dvd : DecidableRel Dvd.dvd] [DecidableEq R] {a : R} {b : R} {n : ℕ} (ha : Irreducible a) (hb : b ≠ 0) : ↑n ≤ multiplicity a b ↔ Multiset.replicate n (normalize a) ≤ UniqueFactorizationMonoid.normalizedFactors b

theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [dec_dvd : DecidableRel Dvd.dvd] [DecidableEq R] {a : R} {b : R} (ha : Irreducible a) (hb : b ≠ 0) : multiplicity a b = ↑(Multiset.count (normalize a) (UniqueFactorizationMonoid.normalizedFactors b))

The multiplicity of an irreducible factor of a nonzero element is exactly the number of times the normalized factor occurs in the normalizedFactors.

See also count_normalizedFactors_eq which expands the definition of multiplicity to produce a specification for count (normalizedFactors _) _..

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [DecidableEq R] {p : R} {x : R} (hp : Irreducible p) (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) : Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

The number of times an irreducible factor p appears in normalizedFactors x is defined by the number of times it divides x.

See also multiplicity_eq_count_normalizedFactors if n is given by multiplicity p x.

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq' {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [DecidableEq R] {p : R} {x : R} (hp : p = 0 ∨ Irreducible p) (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) : Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

The number of times an irreducible factor p appears in normalizedFactors x is defined by the number of times it divides x. This is a slightly more general version of UniqueFactorizationMonoid.count_normalizedFactors_eq that allows p = 0.

See also multiplicity_eq_count_normalizedFactors if n is given by multiplicity p x.

theorem UniqueFactorizationMonoid.max_power_factor {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [dec_dvd : DecidableRel Dvd.dvd] {a₀ : R} {x : R} (h : a₀ ≠ 0) (hx : Irreducible x) : ∃ (n : ℕ) (a : R), ¬x ∣ a ∧ a₀ = x ^ n * a

theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {s : Finset α} (i : α → ℕ) (p : α) (hps : p ∉ s) (is_prime : ∀ q ∈ insert p s, Prime q) (is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q') (q : α) : q ∣ p ^ i p → (q ∣ Finset.prod s fun (p' : α) => p' ^ i p') → IsUnit q

theorem UniqueFactorizationMonoid.induction_on_prime_power {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (s : Finset α) (i : α → ℕ) (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) (h1 : ∀ {x : α}, IsUnit x → P x) (hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)) : P (Finset.prod s fun (p : α) => p ^ i p)

If P holds for units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on a product of powers of distinct primes.

theorem UniqueFactorizationMonoid.induction_on_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α) (h0 : P 0) (h1 : ∀ {x : α}, IsUnit x → P x) (hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)) : P a

If P holds for 0, units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on all a : α.

theorem UniqueFactorizationMonoid.multiplicative_prime_power {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CancelCommMonoidWithZero β] {f : α → β} (s : Finset α) (i : α → ℕ) (j : α → ℕ) (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) (h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y) : f (Finset.prod s fun (p : α) => p ^ (i p + j p)) = f (Finset.prod s fun (p : α) => p ^ i p) * f (Finset.prod s fun (p : α) => p ^ j p)

If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative on all products of primes.

theorem UniqueFactorizationMonoid.multiplicative_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CancelCommMonoidWithZero β] (f : α → β) (a : α) (b : α) (h0 : f 0 = 0) (h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y) : f (a * b) = f a * f b

If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative everywhere.

theorem UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_left {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} {y : R} {d : R} (h : ∀ (p : R), p ∣ x → p ∣ y → IsUnit p) (h' : y ∣ x * d) : y ∣ d

See also IsCoprime.dvd_of_dvd_mul_left.

theorem UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_right {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} {y : R} {d : R} (h : ∀ (p : R), p ∣ x → p ∣ y → IsUnit p) (h' : y ∣ d * x) : y ∣ d

See also IsCoprime.dvd_of_dvd_mul_right.

theorem UniqueFactorizationMonoid.mul_dvd_of_coprime {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x : R} {y : R} {d : R} (h : ∀ (p : R), p ∣ x → p ∣ y → IsUnit p) (hx : x ∣ d) (hy : y ∣ d) : x * y ∣ d

See also IsCoprime.mul_dvd.

@[reducible]

def Associates.FactorSet (α : Type u) [CancelCommMonoidWithZero α] : 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.

Equations

• Associates.FactorSet α = WithTop (Multiset { a : Associates α // Irreducible a })

theorem Associates.FactorSet.coe_add {α : Type u_1} [CancelCommMonoidWithZero α] {a : Multiset { a : Associates α // Irreducible a }} {b : Multiset { a : Associates α // Irreducible a }} : ↑(a + b) = ↑a + ↑b

theorem Associates.FactorSet.sup_add_inf_eq_add {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] (a : Associates.FactorSet α) (b : Associates.FactorSet α) : a ⊔ b + a ⊓ b = a + b

def Associates.FactorSet.prod {α : Type u_1} [CancelCommMonoidWithZero α] : Associates.FactorSet α → Associates α

Evaluates the product of a FactorSet to be the product of the corresponding multiset, or 0 if there is none.

Equations

• Associates.FactorSet.prod x = match x with | none => 0 | some s => Multiset.prod (Multiset.map Subtype.val s)

@[simp]

theorem Associates.prod_top {α : Type u_1} [CancelCommMonoidWithZero α] : Associates.FactorSet.prod ⊤ = 0

@[simp]

theorem Associates.prod_coe {α : Type u_1} [CancelCommMonoidWithZero α] {s : Multiset { a : Associates α // Irreducible a }} : Associates.FactorSet.prod ↑s = Multiset.prod (Multiset.map Subtype.val s)

@[simp]

theorem Associates.prod_add {α : Type u_1} [CancelCommMonoidWithZero α] (a : Associates.FactorSet α) (b : Associates.FactorSet α) : Associates.FactorSet.prod (a + b) = Associates.FactorSet.prod a * Associates.FactorSet.prod b

theorem Associates.prod_mono {α : Type u_1} [CancelCommMonoidWithZero α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} : a ≤ b → Associates.FactorSet.prod a ≤ Associates.FactorSet.prod b

theorem Associates.FactorSet.prod_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (p : Associates.FactorSet α) : Associates.FactorSet.prod p = 0 ↔ p = ⊤

def Associates.bcount {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] (p : { a : Associates α // Irreducible a }) : Associates.FactorSet α → ℕ

bcount p s is the multiplicity of p in the FactorSet s (with bundled p)

Equations

• Associates.bcount p x = match x with | none => 0 | some s => Multiset.count p s

def Associates.count {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] (p : Associates α) : Associates.FactorSet α → ℕ

count p s is the multiplicity of the irreducible p in the FactorSet s.

If p is not irreducible, count p s is defined to be 0.

Equations

• Associates.count p = if hp : Irreducible p then Associates.bcount { val := p, property := hp } else 0

@[simp]

theorem Associates.count_some {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} (hp : Irreducible p) (s : Multiset { a : Associates α // Irreducible a }) : Associates.count p (some s) = Multiset.count { val := p, property := hp } s

@[simp]

theorem Associates.count_zero {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} (hp : Irreducible p) : Associates.count p 0 = 0

theorem Associates.count_reducible {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} (hp : ¬Irreducible p) : Associates.count p = 0

def Associates.BfactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] : { a : Associates α // Irreducible a } → Associates.FactorSet α → Prop

membership in a FactorSet (bundled version)

Equations

• Associates.BfactorSetMem x✝ x = match x✝, x with | x, none => True | p, some l => p ∈ l

def Associates.FactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] (p : Associates α) (s : Associates.FactorSet α) : Prop

FactorSetMem p s is the predicate that the irreducible p is a member of s : FactorSet α.

If p is not irreducible, p is not a member of any FactorSet.

Equations

• Associates.FactorSetMem p s = if hp : Irreducible p then Associates.BfactorSetMem { val := p, property := hp } s else False

instance Associates.instMembershipAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZeroFactorSet {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] : Membership (Associates α) (Associates.FactorSet α)

Equations

• Associates.instMembershipAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZeroFactorSet = { mem := Associates.FactorSetMem }

@[simp]

theorem Associates.factorSetMem_eq_mem {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] (p : Associates α) (s : Associates.FactorSet α) : Associates.FactorSetMem p s = (p ∈ s)

theorem Associates.mem_factorSet_top {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} {hp : Irreducible p} : p ∈ ⊤

theorem Associates.mem_factorSet_some {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} {hp : Irreducible p} {l : Multiset { a : Associates α // Irreducible a }} : p ∈ ↑l ↔ { val := p, property := hp } ∈ l

theorem Associates.reducible_not_mem_factorSet {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : ¬Irreducible p) (s : Associates.FactorSet α) : p ∉ s

theorem Associates.unique' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} : (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → Multiset.prod p = Multiset.prod q → p = q

theorem Associates.FactorSet.unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates.FactorSet α} {q : Associates.FactorSet α} (h : Associates.FactorSet.prod p = Associates.FactorSet.prod q) : p = q

theorem Associates.prod_le_prod_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} (hp : ∀ a ∈ p, Irreducible a) (hq : ∀ a ∈ q, Irreducible a) : Multiset.prod p ≤ Multiset.prod q ↔ p ≤ q

noncomputable def Associates.factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] (a : α) : Multiset { a : Associates α // Irreducible a }

This returns the multiset of irreducible factors as a FactorSet, a multiset of irreducible associates WithTop.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Associates.map_subtype_coe_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} : Multiset.map Subtype.val (Associates.factors' a) = Multiset.map Associates.mk (UniqueFactorizationMonoid.factors a)

theorem Associates.factors'_cong {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {b : α} (h : Associated a b) : Associates.factors' a = Associates.factors' b

noncomputable def Associates.factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) : Associates.FactorSet α

This returns the multiset of irreducible factors of an associate as a FactorSet, a multiset of irreducible associates WithTop.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Associates.factors_0 {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] : Associates.factors 0 = ⊤

@[simp]

theorem Associates.factors_mk {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : α) (h : a ≠ 0) : Associates.factors (Associates.mk a) = ↑(Associates.factors' a)

@[simp]

theorem Associates.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) : Associates.FactorSet.prod (Associates.factors a) = a

theorem Associates.prod_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] (s : Associates.FactorSet α) : Associates.factors (Associates.FactorSet.prod s) = s

theorem Associates.factors_subsingleton {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Subsingleton α] {a : Associates α} : Associates.factors a = none

theorem Associates.factors_eq_none_iff_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} : Associates.factors a = none ↔ a = 0

theorem Associates.factors_eq_some_iff_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} : (∃ (s : Multiset { p : Associates α // Irreducible p }), Associates.factors a = some s) ↔ a ≠ 0

theorem Associates.eq_of_factors_eq_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (h : Associates.factors a = Associates.factors b) : a = b

theorem Associates.eq_of_prod_eq_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} (h : Associates.FactorSet.prod a = Associates.FactorSet.prod b) : a = b

theorem Associates.eq_factors_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : Associates α), Irreducible p → Associates.count p (Associates.factors a) = Associates.count p (Associates.factors b)) : Associates.factors a = Associates.factors b

theorem Associates.eq_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : Associates α), Irreducible p → Associates.count p (Associates.factors a) = Associates.count p (Associates.factors b)) : a = b

theorem Associates.count_le_count_of_factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hb : b ≠ 0) (hp : Irreducible p) (h : Associates.factors a ≤ Associates.factors b) : Associates.count p (Associates.factors a) ≤ Associates.count p (Associates.factors b)

@[simp]

theorem Associates.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) (b : Associates α) : Associates.factors (a * b) = Associates.factors a + Associates.factors b

theorem Associates.factors_mono {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} : a ≤ b → Associates.factors a ≤ Associates.factors b

theorem Associates.factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} : Associates.factors a ≤ Associates.factors b ↔ a ≤ b

theorem Associates.count_le_count_of_le {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hb : b ≠ 0) (hp : Irreducible p) (h : a ≤ b) : Associates.count p (Associates.factors a) ≤ Associates.count p (Associates.factors b)

theorem Associates.prod_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} : Associates.FactorSet.prod a ≤ Associates.FactorSet.prod b ↔ a ≤ b

noncomputable instance Associates.instSupAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] : Sup (Associates α)

Equations

• Associates.instSupAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero = { sup := fun (a b : Associates α) => Associates.FactorSet.prod (Associates.factors a ⊔ Associates.factors b) }

noncomputable instance Associates.instInfAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] : Inf (Associates α)

Equations

• Associates.instInfAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero = { inf := fun (a b : Associates α) => Associates.FactorSet.prod (Associates.factors a ⊓ Associates.factors b) }

noncomputable instance Associates.instLatticeAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] : Lattice (Associates α)

Equations

• One or more equations did not get rendered due to their size.

theorem Associates.sup_mul_inf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) (b : Associates α) : (a ⊔ b) * (a ⊓ b) = a * b

theorem Associates.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {p : Associates α} {hp : Irreducible p} (hm : p ∈ Associates.factors a) : p ∣ a

theorem Associates.dvd_of_mem_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {p : Associates α} {hp : Irreducible p} {hz : a ≠ 0} (h_mem : { val := p, property := hp } ∈ Associates.factors' a) : p ∣ Associates.mk a

theorem Associates.mem_factors'_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) : { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ Associates.factors' a

theorem Associates.mem_factors'_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : { val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ Associates.factors' a ↔ p ∣ a

theorem Associates.mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) : Associates.mk p ∈ Associates.factors (Associates.mk a)

theorem Associates.mem_factors_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : Associates.mk p ∈ Associates.factors (Associates.mk a) ↔ p ∣ a

theorem Associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : Associates.mk a ⊓ Associates.mk b ≠ 1) : ∃ (p : α), Prime p ∧ p ∣ a ∧ p ∣ b

theorem Associates.coprime_iff_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {b : α} (ha0 : a ≠ 0) (hb0 : b ≠ 0) : Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

theorem Associates.factors_self {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) : Associates.factors p = some {{ val := p, property := hp }}

theorem Associates.factors_prime_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ℕ) : Associates.factors (p ^ k) = some (Multiset.replicate k { val := p, property := hp })

theorem Associates.prime_pow_dvd_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {m : Associates α} {p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} : p ^ k ≤ m ↔ k ≤ Associates.count p (Associates.factors m)

theorem Associates.le_of_count_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {m : Associates α} {p : Associates α} (h0 : m ≠ 0) (hp : Irreducible p) : Associates.count p (Associates.factors m) ≠ 0 → p ≤ m

theorem Associates.count_ne_zero_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : Associates.count (Associates.mk p) (Associates.factors (Associates.mk a)) ≠ 0 ↔ p ∣ a

theorem Associates.count_self {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) : Associates.count p (Associates.factors p) = 1

theorem Associates.count_eq_zero_of_ne {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {p : Associates α} {q : Associates α} (hp : Irreducible p) (hq : Irreducible q) (h : p ≠ q) : Associates.count p (Associates.factors q) = 0

theorem Associates.count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) : Associates.count p (Associates.factors (a * b)) = Associates.count p (Associates.factors a) + Associates.count p (Associates.factors b)

theorem Associates.count_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {p : Associates α} (hp : Irreducible p) : Associates.count p (Associates.factors a) = 0 ∨ Associates.count p (Associates.factors b) = 0

theorem Associates.count_mul_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) : Associates.count p (Associates.factors a) = 0 ∨ Associates.count p (Associates.factors a) = Associates.count p (Associates.factors (a * b))

theorem Associates.count_mul_of_coprime' {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) : Associates.count p (Associates.factors (a * b)) = Associates.count p (Associates.factors a) ∨ Associates.count p (Associates.factors (a * b)) = Associates.count p (Associates.factors b)

theorem Associates.dvd_count_of_dvd_count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {k : ℕ} (habk : k ∣ Associates.count p (Associates.factors (a * b))) : k ∣ Associates.count p (Associates.factors a)

@[simp]

theorem Associates.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] : Associates.factors 1 = 0

@[simp]

theorem Associates.pow_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} {k : ℕ} : Associates.factors (a ^ k) = k • Associates.factors a

theorem Associates.count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) : Associates.count p (Associates.factors (a ^ k)) = k * Associates.count p (Associates.factors a)

theorem Associates.dvd_count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) : k ∣ Associates.count p (Associates.factors (a ^ k))

theorem Associates.is_pow_of_dvd_count {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {k : ℕ} (hk : ∀ (p : Associates α), Irreducible p → k ∣ Associates.count p (Associates.factors a)) : ∃ (b : Associates α), a = b ^ k

theorem Associates.eq_pow_count_factors_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {p : Associates α} {a : Associates α} (hp : Irreducible p) {n : ℕ} (h : a ∣ p ^ n) : a = p ^ Associates.count p (Associates.factors a)

The only divisors of prime powers are prime powers. See eq_pow_find_of_dvd_irreducible_pow for an explicit expression as a p-power (without using count).

theorem Associates.count_factors_eq_find_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) : Nat.find (_ : ∃ (n : ℕ), (fun (n : ℕ) => a ∣ p ^ n) n) = Associates.count p (Associates.factors a)

theorem Associates.eq_pow_of_mul_eq_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} {b : Associates α} {c : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {k : ℕ} (h : a * b = c ^ k) : ∃ (d : Associates α), a = d ^ k

theorem Associates.eq_pow_find_of_dvd_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) : a = p ^ Nat.find (_ : ∃ (n : ℕ), (fun (n : ℕ) => a ∣ p ^ n) n)

The only divisors of prime powers are prime powers.

noncomputable def UniqueFactorizationMonoid.toGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [DecidableEq α] : GCDMonoid α

toGCDMonoid constructs a GCD monoid out of a unique factorization domain.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def UniqueFactorizationMonoid.toNormalizedGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq (Associates α)] [DecidableEq α] : NormalizedGCDMonoid α

toNormalizedGCDMonoid constructs a GCD monoid out of a normalization on a unique factorization domain.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def UniqueFactorizationMonoid.fintypeSubtypeDvd {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Fintype Mˣ] (y : M) (hy : y ≠ 0) : Fintype { x : M // x ∣ y }

If y is a nonzero element of a unique factorization monoid with finitely many units (e.g. ℤ, Ideal (ring_of_integers K)), it has finitely many divisors.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def factorization {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] (n : α) : α →₀ ℕ

This returns the multiset of irreducible factors as a Finsupp.

Equations

• factorization n = Multiset.toFinsupp (UniqueFactorizationMonoid.normalizedFactors n)

theorem factorization_eq_count {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {n : α} {p : α} : (factorization n) p = Multiset.count p (UniqueFactorizationMonoid.normalizedFactors n)

@[simp]

theorem factorization_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] : factorization 0 = 0

@[simp]

theorem factorization_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] : factorization 1 = 0

@[simp]

theorem support_factorization {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {n : α} : (factorization n).support = Multiset.toFinset (UniqueFactorizationMonoid.normalizedFactors n)

The support of factorization n is exactly the Finset of normalized factors

@[simp]

theorem factorization_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) : factorization (a * b) = factorization a + factorization b

For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

theorem factorization_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {x : α} {n : ℕ} : factorization (x ^ n) = n • factorization x

For any p, the power of p in x^n is n times the power in x

theorem associated_of_factorization_eq {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] (a : α) (b : α) (ha : a ≠ 0) (hb : b ≠ 0) (h : factorization a = factorization b) : Associated a b