ring_theory.unique_factorization_domain

@[class]

structure wf_dvd_monoid (α : Type u_2) [comm_monoid_with_zero α] :

Prop

well_founded_dvd_not_unit : well_founded dvd_not_unit

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.

Instances of this typeclass

source

@[protected, instance]

def is_noetherian_ring.wf_dvd_monoid {α : Type u_1} [comm_ring α] [is_domain α] [is_noetherian_ring α] :

wf_dvd_monoid α

source

theorem wf_dvd_monoid.of_wf_dvd_monoid_associates {α : Type u_1} [comm_monoid_with_zero α] (h : wf_dvd_monoid (associates α)) :

wf_dvd_monoid α

source

@[protected, instance]

def wf_dvd_monoid.wf_dvd_monoid_associates {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] :

wf_dvd_monoid (associates α)

source

theorem wf_dvd_monoid.well_founded_associates {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] :

well_founded has_lt.lt

source

theorem wf_dvd_monoid.exists_irreducible_factor {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] {a : α} (ha : ¬is_unit a) (ha0 : a ≠ 0) :

∃ (i : α), irreducible i ∧ i ∣ a

source

theorem wf_dvd_monoid.induction_on_irreducible {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] {P : α → Prop} (a : α) (h0 : P 0) (hu : ∀ (u : α), is_unit u → P u) (hi : ∀ (a i : α), a ≠ 0 → irreducible i → P a → P (i * a)) :

P a

source

theorem wf_dvd_monoid.exists_factors {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] (a : α) :

a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → irreducible b) ∧ associated f.prod a)

source

theorem wf_dvd_monoid.not_unit_iff_exists_factors_eq {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] (a : α) (hn0 : a ≠ 0) :

¬is_unit a ↔ ∃ (f : multiset α), (∀ (b : α), b ∈ f → irreducible b) ∧ f.prod = a ∧ f ≠ ∅

source

theorem wf_dvd_monoid.of_well_founded_associates {α : Type u_1} [cancel_comm_monoid_with_zero α] (h : well_founded has_lt.lt) :

wf_dvd_monoid α

source

theorem wf_dvd_monoid.iff_well_founded_associates {α : Type u_1} [cancel_comm_monoid_with_zero α] :

wf_dvd_monoid α ↔ well_founded has_lt.lt

source

@[class]

structure unique_factorization_monoid (α : Type u_2) [cancel_comm_monoid_with_zero α] :

Prop

to_wf_dvd_monoid : wf_dvd_monoid α
irreducible_iff_prime : ∀ {a : α}, irreducible a ↔ prime a

unique factorization monoids.

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

Instances of this typeclass

source

@[reducible]

theorem ufm_of_gcd_of_wf_dvd_monoid {α : Type u_1} [cancel_comm_monoid_with_zero α] [wf_dvd_monoid α] [gcd_monoid α] :

unique_factorization_monoid α

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

source

@[protected, instance]

def associates.ufm {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] :

unique_factorization_monoid (associates α)

source

theorem unique_factorization_monoid.exists_prime_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] (a : α) :

a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)

source

theorem unique_factorization_monoid.induction_on_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), is_unit x → P x) (h₃ : ∀ (a p : α), a ≠ 0 → prime p → P a → P (p * a)) :

P a

source

theorem prime_factors_unique {α : Type u_1} [cancel_comm_monoid_with_zero α] {f g : multiset α} :

(∀ (x : α), x ∈ f → prime x) → (∀ (x : α), x ∈ g → prime x) → associated f.prod g.prod → multiset.rel associated f g

source

theorem unique_factorization_monoid.factors_unique {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {f g : multiset α} (hf : ∀ (x : α), x ∈ f → irreducible x) (hg : ∀ (x : α), x ∈ g → irreducible x) (h : associated f.prod g.prod) :

multiset.rel associated f g

source

theorem prime_factors_irreducible {α : Type u_1} [cancel_comm_monoid_with_zero α] {a : α} {f : multiset α} (ha : irreducible a) (pfa : (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a) :

∃ (p : α), associated a p ∧ f = {p}

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

source

theorem wf_dvd_monoid.of_exists_prime_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] (pf : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)) :

wf_dvd_monoid α

source

theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] (pf : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)) {p : α} :

irreducible p ↔ prime p

source

theorem unique_factorization_monoid.of_exists_prime_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] (pf : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)) :

unique_factorization_monoid α

source

theorem unique_factorization_monoid.iff_exists_prime_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] :

unique_factorization_monoid α ↔ ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)

source

theorem mul_equiv.unique_factorization_monoid {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [cancel_comm_monoid_with_zero β] (e : α ≃* β) (hα : unique_factorization_monoid α) :

unique_factorization_monoid β

source

theorem mul_equiv.unique_factorization_monoid_iff {α : Type u_1} {β : Type u_2} [cancel_comm_monoid_with_zero α] [cancel_comm_monoid_with_zero β] (e : α ≃* β) :

unique_factorization_monoid α ↔ unique_factorization_monoid β

source

theorem irreducible_iff_prime_of_exists_unique_irreducible_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] (eif : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → irreducible b) ∧ associated f.prod a)) (uif : ∀ (f g : multiset α), (∀ (x : α), x ∈ f → irreducible x) → (∀ (x : α), x ∈ g → irreducible x) → associated f.prod g.prod → multiset.rel associated f g) (p : α) :

irreducible p ↔ prime p

source

theorem unique_factorization_monoid.of_exists_unique_irreducible_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] (eif : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → irreducible b) ∧ associated f.prod a)) (uif : ∀ (f g : multiset α), (∀ (x : α), x ∈ f → irreducible x) → (∀ (x : α), x ∈ g → irreducible x) → associated f.prod g.prod → multiset.rel associated f g) :

unique_factorization_monoid α

source

noncomputable def unique_factorization_monoid.factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] (a : α) :

multiset α

Noncomputably determines the multiset of prime factors.

Equations

unique_factorization_monoid.factors a = dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0), classical.some _)

source

theorem unique_factorization_monoid.factors_prod {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {a : α} (ane0 : a ≠ 0) :

associated (unique_factorization_monoid.factors a).prod a

source

theorem unique_factorization_monoid.ne_zero_of_mem_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {p a : α} (h : p ∈ unique_factorization_monoid.factors a) :

a ≠ 0

source

theorem unique_factorization_monoid.dvd_of_mem_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {p a : α} (h : p ∈ unique_factorization_monoid.factors a) :

p ∣ a

source

theorem unique_factorization_monoid.prime_of_factor {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {a : α} (x : α) (hx : x ∈ unique_factorization_monoid.factors a) :

prime x

source

theorem unique_factorization_monoid.irreducible_of_factor {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {a : α} (x : α) :

x ∈ unique_factorization_monoid.factors a → irreducible x

source

@[simp]

theorem unique_factorization_monoid.factors_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] :

unique_factorization_monoid.factors 0 = 0

source

@[simp]

theorem unique_factorization_monoid.factors_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] :

unique_factorization_monoid.factors 1 = 0

source

theorem unique_factorization_monoid.exists_mem_factors_of_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) :

p ∣ a → (∃ (q : α) (H : q ∈ unique_factorization_monoid.factors a), associated p q)

source

theorem unique_factorization_monoid.exists_mem_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {x : α} (hx : x ≠ 0) (h : ¬is_unit x) :

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

source

theorem unique_factorization_monoid.factors_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :

multiset.rel associated (unique_factorization_monoid.factors (x * y)) (unique_factorization_monoid.factors x + unique_factorization_monoid.factors y)

source

theorem unique_factorization_monoid.factors_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] {x : α} (n : ℕ) :

multiset.rel associated (unique_factorization_monoid.factors (x ^ n)) (n • unique_factorization_monoid.factors x)

source

@[simp]

theorem unique_factorization_monoid.factors_pos {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [unique_factorization_monoid α] (x : α) (hx : x ≠ 0) :

0 < unique_factorization_monoid.factors x ↔ ¬is_unit x

source

noncomputable def unique_factorization_monoid.normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] (a : α) :

multiset α

Noncomputably determines the multiset of prime factors.

Equations

unique_factorization_monoid.normalized_factors a = multiset.map ⇑normalize (unique_factorization_monoid.factors a)

source

@[simp]

theorem unique_factorization_monoid.factors_eq_normalized_factors {M : Type u_1} [cancel_comm_monoid_with_zero M] [decidable_eq M] [unique_factorization_monoid M] [unique Mˣ] (x : M) :

unique_factorization_monoid.factors x = unique_factorization_monoid.normalized_factors 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.

source

theorem unique_factorization_monoid.normalized_factors_prod {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a : α} (ane0 : a ≠ 0) :

associated (unique_factorization_monoid.normalized_factors a).prod a

source

theorem unique_factorization_monoid.prime_of_normalized_factor {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a : α} (x : α) :

x ∈ unique_factorization_monoid.normalized_factors a → prime x

source

theorem unique_factorization_monoid.irreducible_of_normalized_factor {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a : α} (x : α) :

x ∈ unique_factorization_monoid.normalized_factors a → irreducible x

source

theorem unique_factorization_monoid.normalize_normalized_factor {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a : α} (x : α) :

x ∈ unique_factorization_monoid.normalized_factors a → ⇑normalize x = x

source

theorem unique_factorization_monoid.normalized_factors_irreducible {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a : α} (ha : irreducible a) :

unique_factorization_monoid.normalized_factors a = {⇑normalize a}

source

theorem unique_factorization_monoid.normalized_factors_eq_of_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] (a p : α) (H : p ∈ unique_factorization_monoid.normalized_factors a) (q : α) (H_1 : q ∈ unique_factorization_monoid.normalized_factors a) :

p ∣ q → p = q

source

theorem unique_factorization_monoid.exists_mem_normalized_factors_of_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) :

p ∣ a → (∃ (q : α) (H : q ∈ unique_factorization_monoid.normalized_factors a), associated p q)

source

theorem unique_factorization_monoid.exists_mem_normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {x : α} (hx : x ≠ 0) (h : ¬is_unit x) :

∃ (p : α), p ∈ unique_factorization_monoid.normalized_factors x

source

@[simp]

theorem unique_factorization_monoid.normalized_factors_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] :

unique_factorization_monoid.normalized_factors 0 = 0

source

@[simp]

theorem unique_factorization_monoid.normalized_factors_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] :

unique_factorization_monoid.normalized_factors 1 = 0

source

@[simp]

theorem unique_factorization_monoid.normalized_factors_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :

unique_factorization_monoid.normalized_factors (x * y) = unique_factorization_monoid.normalized_factors x + unique_factorization_monoid.normalized_factors y

source

@[simp]

theorem unique_factorization_monoid.normalized_factors_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {x : α} (n : ℕ) :

unique_factorization_monoid.normalized_factors (x ^ n) = n • unique_factorization_monoid.normalized_factors x

source

theorem irreducible.normalized_factors_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {p : α} (hp : irreducible p) (k : ℕ) :

unique_factorization_monoid.normalized_factors (p ^ k) = multiset.replicate k (⇑normalize p)

source

theorem unique_factorization_monoid.normalized_factors_prod_eq {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] (s : multiset α) (hs : ∀ (a : α), a ∈ s → irreducible a) :

unique_factorization_monoid.normalized_factors s.prod = multiset.map ⇑normalize s

source

theorem unique_factorization_monoid.dvd_iff_normalized_factors_le_normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :

x ∣ y ↔ unique_factorization_monoid.normalized_factors x ≤ unique_factorization_monoid.normalized_factors y

source

theorem unique_factorization_monoid.associated_iff_normalized_factors_eq_normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :

associated x y ↔ unique_factorization_monoid.normalized_factors x = unique_factorization_monoid.normalized_factors y

source

theorem unique_factorization_monoid.normalized_factors_of_irreducible_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {p : α} (hp : irreducible p) (k : ℕ) :

unique_factorization_monoid.normalized_factors (p ^ k) = multiset.replicate k (⇑normalize p)

source

theorem unique_factorization_monoid.zero_not_mem_normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] (x : α) :

0 ∉ unique_factorization_monoid.normalized_factors x

source

theorem unique_factorization_monoid.dvd_of_mem_normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a p : α} (H : p ∈ unique_factorization_monoid.normalized_factors a) :

p ∣ a

source

theorem unique_factorization_monoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {p r : α} (h : ∀ {m : α}, m ∈ unique_factorization_monoid.normalized_factors r → m = p) (hr : r ≠ 0) :

∃ (i : ℕ), associated (p ^ i) r

source

theorem unique_factorization_monoid.normalized_factors_prod_of_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] [nontrivial α] [unique αˣ] {m : multiset α} (h : ∀ (p : α), p ∈ m → prime p) :

unique_factorization_monoid.normalized_factors m.prod = m

source

theorem unique_factorization_monoid.mem_normalized_factors_eq_of_associated {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {a b c : α} (ha : a ∈ unique_factorization_monoid.normalized_factors c) (hb : b ∈ unique_factorization_monoid.normalized_factors c) (h : associated a b) :

a = b

source

@[simp]

theorem unique_factorization_monoid.normalized_factors_pos {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] (x : α) (hx : x ≠ 0) :

0 < unique_factorization_monoid.normalized_factors x ↔ ¬is_unit x

source

theorem unique_factorization_monoid.dvd_not_unit_iff_normalized_factors_lt_normalized_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq α] [normalization_monoid α] [unique_factorization_monoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :

dvd_not_unit x y ↔ unique_factorization_monoid.normalized_factors x < unique_factorization_monoid.normalized_factors y

source

@[protected]

noncomputable def unique_factorization_monoid.normalization_monoid {α : Type u_1} [cancel_comm_monoid_with_zero α] [nontrivial α] [unique_factorization_monoid α] :

normalization_monoid α

Noncomputably defines a normalization_monoid structure on a unique_factorization_monoid.

Equations

unique_factorization_monoid.normalization_monoid = normalization_monoid_of_monoid_hom_right_inverse {to_fun := λ (a : associates α), ite (a = 0) 0 (multiset.map (classical.some unique_factorization_monoid.normalization_monoid._proof_1) (unique_factorization_monoid.normalized_factors a)).prod, map_one' := _, map_mul' := _} unique_factorization_monoid.normalization_monoid._proof_4

source

@[protected, instance]

noncomputable def unique_factorization_monoid.normalization_monoid.inhabited {α : Type u_1} [cancel_comm_monoid_with_zero α] [nontrivial α] [unique_factorization_monoid α] :

inhabited (normalization_monoid α)

Equations

unique_factorization_monoid.normalization_monoid.inhabited = {default := unique_factorization_monoid.normalization_monoid _inst_3}

source

theorem unique_factorization_monoid.no_factors_of_no_prime_factors {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] {a b : R} (ha : a ≠ 0) (h : ∀ {d : R}, d ∣ a → d ∣ b → ¬prime d) {d : R} :

d ∣ a → d ∣ b → is_unit d

source

theorem unique_factorization_monoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] {a b 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 is_coprime.dvd_of_dvd_mul_left.

source

theorem unique_factorization_monoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] {a b c : R} (ha : a ≠ 0) (no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬prime d) :

a ∣ b * c → a ∣ c

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

source

theorem unique_factorization_monoid.exists_reduced_factors {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] (a : R) (H : a ≠ 0) (b : R) :

∃ (a' b' c' : R), (∀ {d : R}, d ∣ a' → d ∣ b' → is_unit 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.

source

theorem unique_factorization_monoid.exists_reduced_factors' {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] (a b : R) (hb : b ≠ 0) :

∃ (a' b' c' : R), (∀ {d : R}, d ∣ a' → d ∣ b' → is_unit d) ∧ c' * a' = a ∧ c' * b' = b

source

theorem unique_factorization_monoid.pow_right_injective {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] {a : R} (ha0 : a ≠ 0) (ha1 : ¬is_unit a) :

function.injective (has_pow.pow a)

source

theorem unique_factorization_monoid.pow_eq_pow_iff {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] {a : R} (ha0 : a ≠ 0) (ha1 : ¬is_unit a) {i j : ℕ} :

a ^ i = a ^ j ↔ i = j

source

theorem unique_factorization_monoid.le_multiplicity_iff_replicate_le_normalized_factors {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] [nontrivial R] [normalization_monoid R] [dec_dvd : decidable_rel has_dvd.dvd] [decidable_eq R] {a b : R} {n : ℕ} (ha : irreducible a) (hb : b ≠ 0) :

↑n ≤ multiplicity a b ↔ multiset.replicate n (⇑normalize a) ≤ unique_factorization_monoid.normalized_factors b

source

theorem unique_factorization_monoid.multiplicity_eq_count_normalized_factors {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] [nontrivial R] [normalization_monoid R] [dec_dvd : decidable_rel has_dvd.dvd] [decidable_eq R] {a b : R} (ha : irreducible a) (hb : b ≠ 0) :

multiplicity a b = ↑(multiset.count (⇑normalize a) (unique_factorization_monoid.normalized_factors b))

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

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

source

theorem unique_factorization_monoid.count_normalized_factors_eq {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] [nontrivial R] [normalization_monoid R] [decidable_eq R] {p x : R} (hp : irreducible p) (hnorm : ⇑normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) :

multiset.count p (unique_factorization_monoid.normalized_factors x) = n

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

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

source

theorem unique_factorization_monoid.count_normalized_factors_eq' {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] [nontrivial R] [normalization_monoid R] [decidable_eq R] {p x : R} (hp : p = 0 ∨ irreducible p) (hnorm : ⇑normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) :

multiset.count p (unique_factorization_monoid.normalized_factors x) = n

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

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

source

theorem unique_factorization_monoid.max_power_factor {R : Type u_2} [cancel_comm_monoid_with_zero R] [unique_factorization_monoid R] [nontrivial R] [normalization_monoid R] {a₀ x : R} (h : a₀ ≠ 0) (hx : irreducible x) :

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

source

theorem unique_factorization_monoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [decidable_eq α] {s : finset α} (i : α → ℕ) (p : α) (hps : p ∉ s) (is_prime : ∀ (q : α), q ∈ has_insert.insert p s → prime q) (is_coprime : ∀ (q : α), q ∈ has_insert.insert p s → ∀ (q' : α), q' ∈ has_insert.insert p s → q ∣ q' → q = q') (q : α) :

q ∣ p ^ i p → q ∣ s.prod (λ (p' : α), p' ^ i p') → is_unit q

source

theorem unique_factorization_monoid.induction_on_prime_power {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {P : α → Prop} (s : finset α) (i : α → ℕ) (is_prime : ∀ (p : α), p ∈ s → prime p) (is_coprime : ∀ (p : α), p ∈ s → ∀ (q : α), q ∈ s → p ∣ q → p = q) (h1 : ∀ {x : α}, is_unit x → P x) (hpr : ∀ {p : α} (i : ℕ), prime p → P (p ^ i)) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → is_unit p) → P x → P y → P (x * y)) :

P (s.prod (λ (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.

source

theorem unique_factorization_monoid.induction_on_coprime {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {P : α → Prop} (a : α) (h0 : P 0) (h1 : ∀ {x : α}, is_unit x → P x) (hpr : ∀ {p : α} (i : ℕ), prime p → P (p ^ i)) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → is_unit 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 : α.

source

theorem unique_factorization_monoid.multiplicative_prime_power {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {β : Type u_3} [cancel_comm_monoid_with_zero β] {f : α → β} (s : finset α) (i j : α → ℕ) (is_prime : ∀ (p : α), p ∈ s → prime p) (is_coprime : ∀ (p : α), p ∈ s → ∀ (q : α), q ∈ s → p ∣ q → p = q) (h1 : ∀ {x y : α}, is_unit 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 → is_unit p) → f (x * y) = f x * f y) :

f (s.prod (λ (p : α), p ^ (i p + j p))) = f (s.prod (λ (p : α), p ^ i p)) * f (s.prod (λ (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.

source

theorem unique_factorization_monoid.multiplicative_of_coprime {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {β : Type u_3} [cancel_comm_monoid_with_zero β] (f : α → β) (a b : α) (h0 : f 0 = 0) (h1 : ∀ {x y : α}, is_unit 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 → is_unit 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.

source

@[reducible]

def associates.factor_set (α : Type u) [cancel_comm_monoid_with_zero α] :

Type u

factor_set α representation elements of unique factorization domain as multisets. multiset α produced by normalized_factors are only unique up to associated elements, while the multisets in factor_set α 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 struture. Infimum is the greatest common divisor and supremum is the least common multiple.

Equations

associates.factor_set α = with_top (multiset {a // irreducible a})

source

theorem associates.factor_set.coe_add {α : Type u_1} [cancel_comm_monoid_with_zero α] {a b : multiset {a // irreducible a}} :

↑(a + b) = ↑a + ↑b

source

theorem associates.factor_set.sup_add_inf_eq_add {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq (associates α)] (a b : associates.factor_set α) :

a ⊔ b + a ⊓ b = a + b

source

def associates.factor_set.prod {α : Type u_1} [cancel_comm_monoid_with_zero α] :

associates.factor_set α → associates α

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

Equations

associates.factor_set.prod (option.some s) = (multiset.map coe s).prod
associates.factor_set.prod option.none = 0

source

@[simp]

theorem associates.prod_top {α : Type u_1} [cancel_comm_monoid_with_zero α] :

⊤.prod = 0

source

@[simp]

theorem associates.prod_coe {α : Type u_1} [cancel_comm_monoid_with_zero α] {s : multiset {a // irreducible a}} :

↑s.prod = (multiset.map coe s).prod

source

@[simp]

theorem associates.prod_add {α : Type u_1} [cancel_comm_monoid_with_zero α] (a b : associates.factor_set α) :

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

source

theorem associates.prod_mono {α : Type u_1} [cancel_comm_monoid_with_zero α] {a b : associates.factor_set α} :

a ≤ b → a.prod ≤ b.prod

source

theorem associates.factor_set.prod_eq_zero_iff {α : Type u_1} [cancel_comm_monoid_with_zero α] [nontrivial α] (p : associates.factor_set α) :

p.prod = 0 ↔ p = ⊤

source

def associates.bcount {α : Type u_1} [cancel_comm_monoid_with_zero α] [decidable_eq (associates α)] (p : {a // irreducible a}) :

associates.factor_set α → ℕ

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

Equations

associates.bcount p (option.some s) = multiset.count p s
associates.bcount p option.none = 0

source

def associates.count {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] (p : associates α) :

associates.factor_set α → ℕ

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

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

Equations

p.count = dite (irreducible p) (λ (hp : irreducible p), associates.bcount ⟨p, hp⟩) (λ (hp : ¬irreducible p), 0)

source

@[simp]

theorem associates.count_some {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] {p : associates α} (hp : irreducible p) (s : multiset {a // irreducible a}) :

p.count (option.some s) = multiset.count ⟨p, hp⟩ s

source

@[simp]

theorem associates.count_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] {p : associates α} (hp : irreducible p) :

p.count 0 = 0

source

theorem associates.count_reducible {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] {p : associates α} (hp : ¬irreducible p) :

p.count = 0

source

def associates.bfactor_set_mem {α : Type u_1} [cancel_comm_monoid_with_zero α] :

{a // irreducible a} → associates.factor_set α → Prop

membership in a factor_set (bundled version)

Equations

associates.bfactor_set_mem p (option.some l) = (p ∈ l)
associates.bfactor_set_mem _x ⊤ = true

source

def associates.factor_set_mem {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] (p : associates α) (s : associates.factor_set α) :

Prop

factor_set_mem p s is the predicate that the irreducible p is a member of s : factor_set α.

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

Equations

p.factor_set_mem s = dite (irreducible p) (λ (hp : irreducible p), associates.bfactor_set_mem ⟨p, hp⟩ s) (λ (hp : ¬irreducible p), false)

source

@[protected, instance]

def associates.factor_set.has_mem {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] :

has_mem (associates α) (associates.factor_set α)

Equations

associates.factor_set.has_mem = {mem := associates.factor_set_mem (λ (p : associates α), dec_irr p)}

source

@[simp]

theorem associates.factor_set_mem_eq_mem {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] (p : associates α) (s : associates.factor_set α) :

p.factor_set_mem s = (p ∈ s)

source

theorem associates.mem_factor_set_top {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] {p : associates α} {hp : irreducible p} :

p ∈ ⊤

source

theorem associates.mem_factor_set_some {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] {p : associates α} {hp : irreducible p} {l : multiset {a // irreducible a}} :

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

source

theorem associates.reducible_not_mem_factor_set {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] {p : associates α} (hp : ¬irreducible p) (s : associates.factor_set α) :

p ∉ s

source

theorem associates.unique' {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {p q : multiset (associates α)} :

(∀ (a : associates α), a ∈ p → irreducible a) → (∀ (a : associates α), a ∈ q → irreducible a) → p.prod = q.prod → p = q

source

theorem associates.factor_set.unique {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] {p q : associates.factor_set α} (h : p.prod = q.prod) :

p = q

source

theorem associates.prod_le_prod_iff_le {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] {p q : multiset (associates α)} (hp : ∀ (a : associates α), a ∈ p → irreducible a) (hq : ∀ (a : associates α), a ∈ q → irreducible a) :

p.prod ≤ q.prod ↔ p ≤ q

source

noncomputable def associates.factors' {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] (a : α) :

multiset {a // irreducible a}

This returns the multiset of irreducible factors as a factor_set, a multiset of irreducible associates with_top.

Equations

associates.factors' a = multiset.pmap (λ (a : α) (ha : irreducible a), ⟨associates.mk a, _⟩) (unique_factorization_monoid.factors a) _

source

@[simp]

theorem associates.map_subtype_coe_factors' {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] {a : α} :

multiset.map coe (associates.factors' a) = multiset.map associates.mk (unique_factorization_monoid.factors a)

source

theorem associates.factors'_cong {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] {a b : α} (h : associated a b) :

associates.factors' a = associates.factors' b

source

noncomputable def associates.factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a : associates α) :

associates.factor_set α

This returns the multiset of irreducible factors of an associate as a factor_set, a multiset of irreducible associates with_top.

Equations

a.factors = dite (a = 0) (λ (h : a = 0), ⊤) (λ (h : ¬a = 0), quotient.hrec_on a (λ (x : α) (h : ¬⟦x⟧ = 0), option.some (associates.factors' x)) associates.factors._proof_1 h)

source

@[simp]

theorem associates.factors_0 {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :

0.factors = ⊤

source

@[simp]

theorem associates.factors_mk {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a : α) (h : a ≠ 0) :

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

source

@[simp]

theorem associates.factors_prod {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a : associates α) :

a.factors.prod = a

source

theorem associates.prod_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] (s : associates.factor_set α) :

s.prod.factors = s

source

theorem associates.factors_subsingleton {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [subsingleton α] {a : associates α} :

a.factors = option.none

source

theorem associates.factors_eq_none_iff_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} :

a.factors = option.none ↔ a = 0

source

theorem associates.factors_eq_some_iff_ne_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} :

(∃ (s : multiset {p // irreducible p}), a.factors = option.some s) ↔ a ≠ 0

source

theorem associates.eq_of_factors_eq_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (h : a.factors = b.factors) :

a = b

source

theorem associates.eq_of_prod_eq_prod {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] {a b : associates.factor_set α} (h : a.prod = b.prod) :

a = b

source

theorem associates.eq_factors_of_eq_counts {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a 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

source

theorem associates.eq_of_eq_counts {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : associates α), irreducible p → p.count a.factors = p.count b.factors) :

a = b

source

theorem associates.count_le_count_of_factors_le {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b p : associates α} (hb : b ≠ 0) (hp : irreducible p) (h : a.factors ≤ b.factors) :

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

source

@[simp]

theorem associates.factors_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a b : associates α) :

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

source

theorem associates.factors_mono {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} :

a ≤ b → a.factors ≤ b.factors

source

theorem associates.factors_le {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} :

a.factors ≤ b.factors ↔ a ≤ b

source

theorem associates.count_le_count_of_le {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b p : associates α} (hb : b ≠ 0) (hp : irreducible p) (h : a ≤ b) :

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

source

theorem associates.prod_le {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] {a b : associates.factor_set α} :

a.prod ≤ b.prod ↔ a ≤ b

source

@[protected, instance]

noncomputable def associates.has_sup {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :

has_sup (associates α)

Equations

associates.has_sup = {sup := λ (a b : associates α), (a.factors ⊔ b.factors).prod}

source

@[protected, instance]

noncomputable def associates.has_inf {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :

has_inf (associates α)

Equations

associates.has_inf = {inf := λ (a b : associates α), (a.factors ⊓ b.factors).prod}

source

@[protected, instance]

noncomputable def associates.lattice {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :

lattice (associates α)

Equations

associates.lattice = {sup := has_sup.sup associates.has_sup, le := partial_order.le associates.partial_order, lt := partial_order.lt associates.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf associates.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

theorem associates.sup_mul_inf {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a b : associates α) :

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

source

theorem associates.dvd_of_mem_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : associates α} {hp : irreducible p} (hm : p ∈ a.factors) :

p ∣ a

source

theorem associates.dvd_of_mem_factors' {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] {a : α} {p : associates α} {hp : irreducible p} {hz : a ≠ 0} (h_mem : ⟨p, hp⟩ ∈ associates.factors' a) :

p ∣ associates.mk a

source

theorem associates.mem_factors'_of_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) (hd : p ∣ a) :

⟨associates.mk p, _⟩ ∈ associates.factors' a

source

theorem associates.mem_factors'_iff_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) :

⟨associates.mk p, _⟩ ∈ associates.factors' a ↔ p ∣ a

source

theorem associates.mem_factors_of_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) (hd : p ∣ a) :

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

source

theorem associates.mem_factors_iff_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) :

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

source

theorem associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : associates.mk a ⊓ associates.mk b ≠ 1) :

∃ (p : α), prime p ∧ p ∣ a ∧ p ∣ b

source

theorem associates.coprime_iff_inf_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : α} (ha0 : a ≠ 0) (hb0 : b ≠ 0) :

associates.mk a ⊓ associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬prime d

source

theorem associates.factors_self {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {p : associates α} (hp : irreducible p) :

p.factors = option.some {⟨p, hp⟩}

source

theorem associates.factors_prime_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {p : associates α} (hp : irreducible p) (k : ℕ) :

(p ^ k).factors = option.some (multiset.replicate k ⟨p, hp⟩)

source

theorem associates.prime_pow_dvd_iff_le {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {m p : associates α} (h₁ : m ≠ 0) (h₂ : irreducible p) {k : ℕ} :

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

source

theorem associates.le_of_count_ne_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {m p : associates α} (h0 : m ≠ 0) (hp : irreducible p) :

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

source

theorem associates.count_ne_zero_iff_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} (ha0 : a ≠ 0) (hp : irreducible p) :

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

source

theorem associates.count_self {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {p : associates α} (hp : irreducible p) :

p.count p.factors = 1

source

theorem associates.count_eq_zero_of_ne {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {p q : associates α} (hp : irreducible p) (hq : irreducible q) (h : p ≠ q) :

p.count q.factors = 0

source

theorem associates.count_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {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

source

theorem associates.count_of_coprime {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (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) :

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

source

theorem associates.count_mul_of_coprime {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a 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

source

theorem associates.count_mul_of_coprime' {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b 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

source

theorem associates.dvd_count_of_dvd_count_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a 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

source

@[simp]

theorem associates.factors_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] :

1.factors = 0

source

@[simp]

theorem associates.pow_factors {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {a : associates α} {k : ℕ} :

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

source

theorem associates.count_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {a : associates α} (ha : a ≠ 0) {p : associates α} (hp : irreducible p) (k : ℕ) :

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

source

theorem associates.dvd_count_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {a : associates α} (ha : a ≠ 0) {p : associates α} (hp : irreducible p) (k : ℕ) :

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

source

theorem associates.is_pow_of_dvd_count {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {a : associates α} (ha : a ≠ 0) {k : ℕ} (hk : ∀ (p : associates α), irreducible p → k ∣ p.count a.factors) :

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

source

theorem associates.eq_pow_count_factors_of_dvd_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {p 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).

source

theorem associates.count_factors_eq_find_of_dvd_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : associates α} (hp : irreducible p) [Π (n : ℕ), decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) :

nat.find _ = p.count a.factors

source

theorem associates.eq_pow_of_mul_eq_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] {a b 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

source

theorem associates.eq_pow_find_of_dvd_irreducible_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] {a 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.

source

theorem associates.quot_out {α : Type u_1} [comm_monoid α] (a : associates α) :

associates.mk (quot.out a) = a

source

noncomputable def unique_factorization_monoid.to_gcd_monoid (α : Type u_1) [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [decidable_eq (associates α)] [decidable_eq α] :

gcd_monoid α

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

Equations

unique_factorization_monoid.to_gcd_monoid α = {gcd := λ (a b : α), quot.out (associates.mk a ⊓ associates.mk b), lcm := λ (a b : α), quot.out (associates.mk a ⊔ associates.mk b), gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}

source

noncomputable def unique_factorization_monoid.to_normalized_gcd_monoid (α : Type u_1) [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq (associates α)] [decidable_eq α] :

normalized_gcd_monoid α

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

Equations

unique_factorization_monoid.to_normalized_gcd_monoid α = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit _inst_3, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}, to_gcd_monoid := {gcd := λ (a b : α), (associates.mk a ⊓ associates.mk b).out, lcm := λ (a b : α), (associates.mk a ⊔ associates.mk b).out, gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}, normalize_gcd := _, normalize_lcm := _}

source

noncomputable def unique_factorization_monoid.fintype_subtype_dvd {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique_factorization_monoid M] [fintype Mˣ] (y : M) (hy : y ≠ 0) :

fintype {x // 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

unique_factorization_monoid.fintype_subtype_dvd y hy = fintype.of_finset (finset.image (λ (s : multiset M × Mˣ), ↑(s.snd) * s.fst.prod) ((unique_factorization_monoid.normalized_factors y).powerset.to_finset ×ˢ finset.univ)) _

source

noncomputable def factorization {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] (n : α) :

α →₀ ℕ

This returns the multiset of irreducible factors as a finsupp

Equations

factorization n = ⇑multiset.to_finsupp (unique_factorization_monoid.normalized_factors n)

source

theorem factorization_eq_count {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] {n p : α} :

⇑(factorization n) p = multiset.count p (unique_factorization_monoid.normalized_factors n)

source

@[simp]

theorem factorization_zero {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] :

factorization 0 = 0

source

@[simp]

theorem factorization_one {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] :

factorization 1 = 0

source

@[simp]

theorem support_factorization {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] {n : α} :

(factorization n).support = (unique_factorization_monoid.normalized_factors n).to_finset

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

source

@[simp]

theorem factorization_mul {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] {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

source

theorem factorization_pow {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] {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

source

theorem associated_of_factorization_eq {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique_factorization_monoid α] [normalization_monoid α] [decidable_eq α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) (h : factorization a = factorization b) :

associated a b

mathlib3 documentation

Unique factorization #

Main Definitions #

To do #