Documentation

theorem wellFounded_dvdNotUnit {α : Type u_2} [CommMonoidWithZero α] [h : WfDvdMonoid α] :

WellFounded DvdNotUnit

@[instance 100]

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

Equations

⋯ = ⋯

theorem WfDvdMonoid.of_wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] :

WfDvdMonoid (Associates α) → WfDvdMonoid α

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

WfDvdMonoid (Associates α)

Equations

⋯ = ⋯

theorem WfDvdMonoid.wellFoundedLT_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] :

WellFoundedLT (Associates α)

@[deprecated WfDvdMonoid.wellFoundedLT_associates]

theorem WfDvdMonoid.wellFounded_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] :

WellFounded fun (x1 x2 : Associates α) => x1 < x2

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 f.prod 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) ∧ 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 z → z ∣ x → ¬z ∣ y) :

IsRelPrime x y

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

@[deprecated WfDvdMonoid.of_wellFoundedLT_associates]

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

theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] :

WfDvdMonoid α ↔ WellFoundedLT (Associates α)

theorem WfDvdMonoid.max_power_factor' {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ : α} {x : α} (h : a₀ ≠ 0) (hx : ¬IsUnit x) :

∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

theorem WfDvdMonoid.max_power_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ : α} {x : α} (h : a₀ ≠ 0) (hx : Irreducible x) :

∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

theorem multiplicity.finite_of_not_isUnit {α : Type u_1} [CancelCommMonoidWithZero α] [WfDvdMonoid α] {a : α} {b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) :

multiplicity.Finite a b

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

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

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

Instances

theorem UniqueFactorizationMonoid.irreducible_iff_prime {α : Type u_2} :

∀ {inst : CancelCommMonoidWithZero α} [self : UniqueFactorizationMonoid α] {a : α}, Irreducible a ↔ Prime a

@[instance 100]

instance ufm_of_decomposition_of_wfDvdMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [WfDvdMonoid α] [DecompositionMonoid α] :

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

Equations

⋯ = ⋯

@[deprecated ufm_of_decomposition_of_wfDvdMonoid]

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

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

UniqueFactorizationMonoid (Associates α)

Equations

⋯ = ⋯

theorem UniqueFactorizationMonoid.exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :

a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a

instance UniqueFactorizationMonoid.instDecompositionMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

DecompositionMonoid α

Equations

⋯ = ⋯

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

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) :

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

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) :

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

Multiset α

Noncomputably determines the multiset of prime factors.

Equations

UniqueFactorizationMonoid.factors a = if h : a = 0 then 0 else Classical.choose ⋯

Instances For

theorem UniqueFactorizationMonoid.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) :

Associated (UniqueFactorizationMonoid.factors a).prod a

@[simp]

theorem UniqueFactorizationMonoid.factors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.factors 0 = 0

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

a ≠ 0

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

p ∣ a

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

Prime x

theorem UniqueFactorizationMonoid.irreducible_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.factors a → Irreducible x

@[simp]

theorem UniqueFactorizationMonoid.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

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 ∈ UniqueFactorizationMonoid.factors a, Associated p q

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

∃ (p : α), p ∈ UniqueFactorizationMonoid.factors x

theorem UniqueFactorizationMonoid.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) :

Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x ^ n)) (n • UniqueFactorizationMonoid.factors x)

@[simp]

theorem UniqueFactorizationMonoid.factors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) :

0 < UniqueFactorizationMonoid.factors x ↔ ¬IsUnit x

theorem UniqueFactorizationMonoid.factors_pow_count_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {x : α} (hx : x ≠ 0) :

Associated (∏ p ∈ (UniqueFactorizationMonoid.factors x).toFinset, p ^ Multiset.count p (UniqueFactorizationMonoid.factors x)) x

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

Multiset.Rel Associated (UniqueFactorizationMonoid.factors a) (UniqueFactorizationMonoid.factors b)

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

Multiset α

Noncomputably determines the multiset of prime factors.

Equations

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

Instances For

UniqueFactorizationMonoid.factors x = UniqueFactorizationMonoid.normalizedFactors x

@[simp]

theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Subsingleton Mˣ] (x : M) :

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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) :

Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a

theorem UniqueFactorizationMonoid.prime_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.normalizedFactors a → Prime x

theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.normalizedFactors a → Irreducible x

theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.normalizedFactors a → normalize x = x

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

UniqueFactorizationMonoid.normalizedFactors a = {normalize a}

theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :

∃ (p : α), p ∈ UniqueFactorizationMonoid.normalizedFactors x

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.normalizedFactors 0 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.normalizedFactors 1 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) :

UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x

theorem Irreducible.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) :

UniqueFactorizationMonoid.normalizedFactors s.prod = Multiset.map (⇑normalize) s

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

x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y

UniqueFactorizationMonoid.normalizedFactors a = UniqueFactorizationMonoid.normalizedFactors b

theorem Associated.normalizedFactors_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} {b : α} (h : Associated a b) :

theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) :

0 ∉ UniqueFactorizationMonoid.normalizedFactors x

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

p ∣ a

theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton αˣ] {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 α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton αˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) :

UniqueFactorizationMonoid.normalizedFactors m.prod = m

theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) :

0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x

theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [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 α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : 0 ∉ s) :

UniqueFactorizationMonoid.normalizedFactors s.prod = (Multiset.map UniqueFactorizationMonoid.normalizedFactors s).sum

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

NormalizationMonoid α

Noncomputably defines a normalizationMonoid structure on a UniqueFactorizationMonoid.

Equations

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

Instances For

theorem UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {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 : R} {b : R} {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 : 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), 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 : R) (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]

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]

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.

theorem UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] {a : R} {b : R} {n : ℕ} (ha : Irreducible a) (hb : b ≠ 0) :

↑n ≤ emultiplicity a b ↔ Multiset.replicate n (normalize a) ≤ UniqueFactorizationMonoid.normalizedFactors b

theorem UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {a : R} {b : R} (ha : Irreducible a) (hb : b ≠ 0) :

emultiplicity 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] [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] [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.

@[deprecated WfDvdMonoid.max_power_factor]

theorem UniqueFactorizationMonoid.max_power_factor {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a₀ : R} {x : R} (h : a₀ ≠ 0) (hx : Irreducible x) :

∃ (n : ℕ) (a : R), ¬x ∣ a ∧ a₀ = x ^ n * a

Deprecated. Use WfDvdMonoid.max_power_factor instead.

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') :

IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')

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 : α}, IsRelPrime x y → P x → P y → P (x * y)) :

P (∏ p ∈ s, 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 : α}, IsRelPrime x y → 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 : α}, IsRelPrime x y → f (x * y) = f x * f y) :

f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, 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 : α}, IsRelPrime x y → 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.

@[reducible, inline]

abbrev 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 })

Instances For

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 none = 0
Associates.FactorSet.prod (some s) = (Multiset.map Subtype.val s).prod

Instances For

@[simp]

theorem Associates.prod_top {α : Type u_1} [CancelCommMonoidWithZero α] :

⊤.prod = 0

@[simp]

theorem Associates.prod_coe {α : Type u_1} [CancelCommMonoidWithZero α] {s : Multiset { a : Associates α // Irreducible a }} :

Associates.FactorSet.prod ↑s = (Multiset.map Subtype.val s).prod

@[simp]

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

(a + b).prod = a.prod * b.prod

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

a ≤ b → a.prod ≤ b.prod

theorem Associates.FactorSet.prod_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (p : Associates.FactorSet α) :

p.prod = 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 none = 0
Associates.bcount p (some s) = Multiset.count p s

Instances For

def Associates.count {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] (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

p.count = if hp : Irreducible p then Associates.bcount ⟨p, hp⟩ else 0

Instances For

@[simp]

theorem Associates.count_some {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : Irreducible p) (s : Multiset { a : Associates α // Irreducible a }) :

p.count ↑s = Multiset.count ⟨p, hp⟩ s

@[simp]

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

p.count 0 = 0

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

p.count = 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 none = True
Associates.BfactorSetMem x (some l) = (x ∈ l)

Instances For

def Associates.FactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] (s : Associates.FactorSet α) (p : Associates α) :

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 s p = if hp : Irreducible p then Associates.BfactorSetMem ⟨p, hp⟩ s else False

Instances For

instance Associates.instMembershipFactorSet {α : Type u_1} [CancelCommMonoidWithZero α] :

Membership (Associates α) (Associates.FactorSet α)

Equations

Associates.instMembershipFactorSet = { mem := Associates.FactorSetMem }

@[simp]

theorem Associates.factorSetMem_eq_mem {α : Type u_1} [CancelCommMonoidWithZero α] (p : Associates α) (s : Associates.FactorSet α) :

Associates.FactorSetMem s p = (p ∈ s)

theorem Associates.mem_factorSet_top {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {hp : Irreducible p} :

p ∈ ⊤

theorem Associates.mem_factorSet_some {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {hp : Irreducible p} {l : Multiset { a : Associates α // Irreducible a }} :

p ∈ ↑l ↔ ⟨p, hp⟩ ∈ l

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

p ∉ s

theorem Associates.irreducible_of_mem_factorSet {α : Type u_1} [CancelCommMonoidWithZero α] {p : Associates α} {s : Associates.FactorSet α} (h : p ∈ s) :

Irreducible p

theorem Associates.unique' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} :

(∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

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

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) :

p.prod ≤ q.prod ↔ p ≤ q

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

Multiset { a : Associates α // Irreducible a }

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

Equations

Associates.factors' a = Multiset.pmap (fun (a : α) (ha : Irreducible a) => ⟨Associates.mk a, ⋯⟩) (UniqueFactorizationMonoid.factors a) ⋯

Instances For

@[simp]

theorem Associates.map_subtype_coe_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} :

Multiset.map Subtype.val (Associates.factors' a) = Multiset.map Associates.mk (UniqueFactorizationMonoid.factors a)

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

Associates.factors' a = Associates.factors' b

noncomputable def Associates.factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (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.

Instances For

@[simp]

theorem Associates.factors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

Associates.factors 0 = ⊤

@[deprecated Associates.factors_zero]

theorem Associates.factors_0 {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

Associates.factors 0 = ⊤

Alias of Associates.factors_zero.

@[simp]

theorem Associates.factors_mk {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) (h : a ≠ 0) :

(Associates.mk a).factors = ↑(Associates.factors' a)

@[simp]

theorem Associates.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) :

a.factors.prod = a

@[simp]

theorem Associates.prod_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] (s : Associates.FactorSet α) :

s.prod.factors = s

theorem Associates.factors_subsingleton {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Subsingleton α] {a : Associates α} :

a.factors = ⊤

theorem Associates.factors_eq_top_iff_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} :

a.factors = ⊤ ↔ a = 0

@[deprecated Associates.factors_eq_top_iff_zero]

theorem Associates.factors_eq_none_iff_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} :

a.factors = ⊤ ↔ a = 0

Alias of Associates.factors_eq_top_iff_zero.

theorem Associates.factors_eq_some_iff_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} :

(∃ (s : Multiset { p : Associates α // Irreducible p }), a.factors = ↑s) ↔ a ≠ 0

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

a = b

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

a = b

@[simp]

theorem Associates.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) (b : Associates α) :

(a * b).factors = a.factors + b.factors

theorem Associates.factors_mono {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {b : Associates α} :

a ≤ b → a.factors ≤ b.factors

@[simp]

theorem Associates.factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {b : Associates α} :

a.factors ≤ b.factors ↔ a ≤ b

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

a.factors = b.factors

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

a = b

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

p.count a.factors ≤ p.count b.factors

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

p.count a.factors ≤ p.count b.factors

theorem Associates.prod_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} :

a.prod ≤ b.prod ↔ a ≤ b

noncomputable instance Associates.instSup {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

Sup (Associates α)

Equations

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

noncomputable instance Associates.instInf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

Inf (Associates α)

Equations

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

noncomputable instance Associates.instLattice {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

Lattice (Associates α)

Equations

Associates.instLattice = Lattice.mk ⋯ ⋯ ⋯

theorem Associates.sup_mul_inf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : Associates α) (b : Associates α) :

(a ⊔ b) * (a ⊓ b) = a * b

theorem Associates.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : Associates α} {p : Associates α} (hm : p ∈ a.factors) :

p ∣ a

theorem Associates.dvd_of_mem_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : Associates α} {hp : Irreducible p} {hz : a ≠ 0} (h_mem : ⟨p, hp⟩ ∈ Associates.factors' a) :

p ∣ Associates.mk a

theorem Associates.mem_factors'_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :

⟨Associates.mk p, ⋯⟩ ∈ Associates.factors' a

theorem Associates.mem_factors'_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

⟨Associates.mk p, ⋯⟩ ∈ Associates.factors' a ↔ p ∣ a

theorem Associates.mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :

Associates.mk p ∈ (Associates.mk a).factors

theorem Associates.mem_factors_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

Associates.mk p ∈ (Associates.mk a).factors ↔ p ∣ a

theorem Associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {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 α] [UniqueFactorizationMonoid α] {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 α] [Nontrivial α] {p : Associates α} (hp : Irreducible p) :

p.factors = ↑{⟨p, hp⟩}

theorem Associates.factors_prime_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ℕ) :

(p ^ k).factors = ↑(Multiset.replicate k ⟨p, hp⟩)

theorem Associates.prime_pow_le_iff_le_bcount {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] {m : Associates α} {p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} :

p ^ k ≤ m ↔ k ≤ Associates.bcount ⟨p, h₂⟩ m.factors

@[simp]

theorem Associates.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] :

Associates.factors 1 = 0

@[simp]

theorem Associates.pow_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {a : Associates α} {k : ℕ} :

(a ^ k).factors = k • a.factors

theorem Associates.prime_pow_dvd_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {m : Associates α} {p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} :

p ^ k ≤ m ↔ k ≤ p.count m.factors

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

p.count m.factors ≠ 0 → p ≤ m

theorem Associates.count_ne_zero_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

(Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a

theorem Associates.count_self {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) :

p.count p.factors = 1

theorem Associates.count_eq_zero_of_ne {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {p : Associates α} {q : Associates α} (hp : Irreducible p) (hq : Irreducible q) (h : p ≠ q) :

p.count q.factors = 0

theorem Associates.count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) :

p.count (a * b).factors = p.count a.factors + p.count b.factors

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

p.count a.factors = 0 ∨ p.count b.factors = 0

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

p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors

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

p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors

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

k ∣ p.count a.factors

theorem Associates.count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) :

p.count (a ^ k).factors = k * p.count a.factors

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

k ∣ p.count (a ^ k).factors

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

∃ (b : Associates α), a = b ^ k

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

a = p ^ p.count a.factors

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 α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [(p : Associates α) → Decidable (Irreducible p)] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) :

Nat.find ⋯ = p.count a.factors

theorem Associates.eq_pow_of_mul_eq_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {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 α] [UniqueFactorizationMonoid α] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) :

a = p ^ Nat.find ⋯

The only divisors of prime powers are prime powers.

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

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.

Instances For

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

NormalizedGCDMonoid α

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

Equations

UniqueFactorizationMonoid.toNormalizedGCDMonoid α = NormalizedGCDMonoid.mk ⋯ ⋯

Instances For

instance instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

Nonempty (NormalizedGCDMonoid α)

Equations

⋯ = ⋯