@[class]
- 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.
@[instance]
@[instance]
theorem
wf_dvd_monoid.of_wf_dvd_monoid_associates
{α : Type u_1}
[comm_monoid_with_zero α]
(h : wf_dvd_monoid (associates α)) :
@[instance]
def
wf_dvd_monoid.wf_dvd_monoid_associates
{α : Type u_1}
[comm_monoid_with_zero α]
[wf_dvd_monoid α] :
theorem
wf_dvd_monoid.well_founded_associates
{α : Type u_1}
[comm_monoid_with_zero α]
[wf_dvd_monoid α] :
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
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
theorem
wf_dvd_monoid.exists_factors
{α : Type u_1}
[comm_monoid_with_zero α]
[wf_dvd_monoid α]
(a : α)
(a_1 : a ≠ 0) :
∃ (f : multiset α), (∀ (b : α), b ∈ f → irreducible b) ∧ associated f.prod a
theorem
wf_dvd_monoid.of_well_founded_associates
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(h : well_founded has_lt.lt) :
@[class]
- to_wf_dvd_monoid : wf_dvd_monoid α
- irreducible_iff_prime : ∀ {a : α}, irreducible a ↔ prime a
unique factorization monoids.
These are defined as comm_cancel_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_unique_irreducible_factorization
To define a UFD using the definition in terms of multisets
of prime factors, use the definition of_exists_prime_factorization
@[instance]
def
ufm_of_gcd_of_wf_dvd_monoid
{α : Type u_1}
[nontrivial α]
[comm_cancel_monoid_with_zero α]
[wf_dvd_monoid α]
[gcd_monoid α] :
@[instance]
def
associates.ufm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α] :
theorem
unique_factorization_monoid.exists_prime_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
(a : α)
(a_1 : a ≠ 0) :
theorem
unique_factorization_monoid.induction_on_prime
{α : Type u_1}
[comm_cancel_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
theorem
unique_factorization_monoid.factors_unique
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
{f g : multiset α}
(a : ∀ (x : α), x ∈ f → irreducible x)
(a_1 : ∀ (x : α), x ∈ g → irreducible x)
(a_2 : associated f.prod g.prod) :
theorem
prime_factors_unique
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{f g : multiset α}
(a : ∀ (x : α), x ∈ f → prime x)
(a_1 : ∀ (x : α), x ∈ g → prime x)
(a_2 : associated f.prod g.prod) :
theorem
prime_factors_irreducible
{α : Type u_1}
[comm_cancel_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 :: 0
If an irreducible has a prime factorization, then it is an associate of one of its prime factors.
theorem
wf_dvd_monoid_of_exists_prime_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(pf : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)) :
theorem
irreducible_iff_prime_of_exists_prime_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(pf : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a))
{p : α} :
irreducible p ↔ prime p
theorem
unique_factorization_monoid_of_exists_prime_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(pf : ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)) :
theorem
unique_factorization_monoid_iff_exists_prime_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α] :
unique_factorization_monoid α ↔ ∀ (a : α), a ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → prime b) ∧ associated f.prod a)
theorem
irreducible_iff_prime_of_exists_unique_irreducible_of_factor
{α : Type u_1}
[comm_cancel_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
theorem
unique_factorization_monoid.of_exists_unique_irreducible_of_factor
{α : Type u_1}
[comm_cancel_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) :
def
unique_factorization_monoid.factors
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[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), multiset.map ⇑normalize (classical.some _))
theorem
unique_factorization_monoid.factors_prod
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a : α}
(ane0 : a ≠ 0) :
theorem
unique_factorization_monoid.prime_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a : α}
(x : α)
(a_1 : x ∈ unique_factorization_monoid.factors a) :
prime x
theorem
unique_factorization_monoid.irreducible_of_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a : α}
(x : α)
(a_1 : x ∈ unique_factorization_monoid.factors a) :
theorem
unique_factorization_monoid.normalize_factor
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a : α}
(x : α)
(a_1 : x ∈ unique_factorization_monoid.factors a) :
theorem
unique_factorization_monoid.factors_irreducible
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a : α}
(ha : irreducible a) :
theorem
unique_factorization_monoid.exists_mem_factors_of_dvd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq α]
[nontrivial α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a p : α}
(ha0 : a ≠ 0)
(hp : irreducible p)
(a_1 : p ∣ a) :
∃ (q : α) (H : q ∈ unique_factorization_monoid.factors a), associated p q
theorem
unique_factorization_monoid.no_factors_of_no_prime_of_factor
{R : Type u_2}
[comm_cancel_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}
(a_1 : d ∣ a)
(a_2 : d ∣ b) :
is_unit d
theorem
unique_factorization_monoid.dvd_of_dvd_mul_left_of_no_prime_of_factor
{R : Type u_2}
[comm_cancel_monoid_with_zero R]
[unique_factorization_monoid R]
{a b c : R}
(ha : a ≠ 0)
(a_1 : ∀ {d : R}, d ∣ a → d ∣ c → ¬prime d)
(a_2 : 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.
theorem
unique_factorization_monoid.dvd_of_dvd_mul_right_of_no_prime_of_factor
{R : Type u_2}
[comm_cancel_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_1 : 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.
theorem
unique_factorization_monoid.exists_reduced_factors
{R : Type u_2}
[comm_cancel_monoid_with_zero R]
[unique_factorization_monoid R]
(a : R)
(H : a ≠ 0)
(b : R) :
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
unique_factorization_monoid.exists_reduced_factors'
{R : Type u_2}
[comm_cancel_monoid_with_zero R]
[unique_factorization_monoid R]
(a b : R)
(hb : b ≠ 0) :
factor_set α representation elements of unique factorization domain as multisets.
multiset α produced by factors are only unique up to associated elements, while the multisets in
factor_set α are unqiue 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})
theorem
associates.factor_set.coe_add
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{a b : multiset {a // irreducible a}} :
theorem
associates.factor_set.sup_add_inf_eq_add
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq (associates α)]
(a b : associates.factor_set α) :
def
associates.factor_set.prod
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(a : associates.factor_set α) :
Evaluates the product of a factor_set to be the product of the corresponding multiset,
or 0 if there is none.
Equations
@[simp]
@[simp]
theorem
associates.prod_coe
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{s : multiset {a // irreducible a}} :
@[simp]
theorem
associates.prod_add
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(a b : associates.factor_set α) :
theorem
associates.prod_mono
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
{a b : associates.factor_set α}
(a_1 : a ≤ b) :
def
associates.bcount
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[decidable_eq (associates α)]
(p : {a // irreducible a})
(a : associates.factor_set α) :
bcount p s is the multiplicity of p in the factor_set s (with bundled p)
Equations
- associates.bcount p (some s) = multiset.count p s
- associates.bcount p none = 0
def
associates.count
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[decidable_eq (associates α)]
(p : associates α)
(a : 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)
@[simp]
theorem
associates.count_some
{α : Type u_1}
[comm_cancel_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 (some s) = multiset.count ⟨p, hp⟩ s
@[simp]
theorem
associates.count_zero
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[decidable_eq (associates α)]
{p : associates α}
(hp : irreducible p) :
theorem
associates.count_reducible
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[decidable_eq (associates α)]
{p : associates α}
(hp : ¬irreducible p) :
def
associates.bfactor_set_mem
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
(a : {a // irreducible a})
(a_1 : associates.factor_set α) :
Prop
membership in a factor_set (bundled version)
Equations
- associates.bfactor_set_mem p (some l) = (p ∈ l)
- associates.bfactor_set_mem _x ⊤ = true
def
associates.factor_set_mem
{α : Type u_1}
[comm_cancel_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)
@[instance]
def
associates.has_mem
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)] :
has_mem (associates α) (associates.factor_set α)
Equations
- associates.has_mem = {mem := associates.factor_set_mem (λ (p : associates α), dec_irr p)}
@[simp]
theorem
associates.factor_set_mem_eq_mem
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
(p : associates α)
(s : associates.factor_set α) :
p.factor_set_mem s = (p ∈ s)
theorem
associates.mem_factor_set_top
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
{p : associates α}
{hp : irreducible p} :
theorem
associates.mem_factor_set_some
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
{p : associates α}
{hp : irreducible p}
{l : multiset {a // irreducible a}} :
theorem
associates.reducible_not_mem_factor_set
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
{p : associates α}
(hp : ¬irreducible p)
(s : associates.factor_set α) :
p ∉ s
theorem
associates.unique'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
{p q : multiset (associates α)}
(a : ∀ (a : associates α), a ∈ p → irreducible a)
(a_1 : ∀ (a : associates α), a ∈ q → irreducible a)
(a_2 : p.prod = q.prod) :
p = q
theorem
associates.prod_le_prod_iff_le
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
{p q : multiset (associates α)}
(hp : ∀ (a : associates α), a ∈ p → irreducible a)
(hq : ∀ (a : associates α), a ∈ q → irreducible a) :
def
associates.factors'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_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) _
@[simp]
theorem
associates.map_subtype_coe_factors'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
{a : α} :
theorem
associates.factors'_cong
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
{a b : α}
(ha : a ≠ 0)
(hb : b ≠ 0)
(h : associated a b) :
def
associates.factors
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
(a : associates α) :
This returns the multiset of irreducible factors of an associate as a factor_set,
a multiset of irreducible associates with_top.
@[simp]
theorem
associates.factors_0
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)] :
@[simp]
theorem
associates.factors_mk
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
(a : α)
(h : a ≠ 0) :
(associates.mk a).factors = ↑(associates.factors' a)
theorem
associates.prod_factors
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
(s : associates.factor_set α) :
@[simp]
theorem
associates.factors_prod
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
(a : associates α) :
theorem
associates.eq_of_factors_eq_factors
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a b : associates α}
(h : a.factors = b.factors) :
a = b
theorem
associates.eq_of_prod_eq_prod
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
{a b : associates.factor_set α}
(h : a.prod = b.prod) :
a = b
@[simp]
theorem
associates.factors_mul
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
(a b : associates α) :
theorem
associates.factors_mono
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a b : associates α}
(a_1 : a ≤ b) :
theorem
associates.factors_le
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a b : associates α} :
theorem
associates.prod_le
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
{a b : associates.factor_set α} :
@[instance]
def
associates.has_sup
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)] :
has_sup (associates α)
Equations
- associates.has_sup = {sup := λ (a b : associates α), (a.factors ⊔ b.factors).prod}
@[instance]
def
associates.has_inf
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)] :
has_inf (associates α)
Equations
- associates.has_inf = {inf := λ (a b : associates α), (a.factors ⊓ b.factors).prod}
@[instance]
def
associates.bounded_lattice
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)] :
Equations
- associates.bounded_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 := _, top := order_top.top associates.order_top, le_top := _, bot := order_bot.bot associates.order_bot, bot_le := _}
theorem
associates.sup_mul_inf
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
(a b : associates α) :
theorem
associates.dvd_of_mem_factors
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a p : associates α}
{hp : irreducible p}
(hm : p ∈ a.factors) :
p ∣ a
theorem
associates.dvd_of_mem_factors'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
{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}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
{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}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
{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}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_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
theorem
associates.mem_factors_iff_dvd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_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
theorem
associates.exists_prime_dvd_of_not_inf_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a b : α}
(ha : a ≠ 0)
(hb : b ≠ 0)
(h : associates.mk a ⊓ associates.mk b ≠ 1) :
theorem
associates.coprime_iff_inf_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_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
theorem
associates.factors_prime_pow
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{p : associates α}
(hp : irreducible p)
(k : ℕ) :
theorem
associates.prime_pow_dvd_iff_le
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{m p : associates α}
(h₁ : m ≠ 0)
(h₂ : irreducible p)
{k : ℕ} :
theorem
associates.le_of_count_ne_zero
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{m p : associates α}
(h0 : m ≠ 0)
(hp : irreducible p)
(a : p.count m.factors ≠ 0) :
p ≤ m
theorem
associates.count_mul
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a : associates α}
(ha : a ≠ 0)
{b : associates α}
(hb : b ≠ 0)
{p : associates α}
(hp : irreducible p) :
theorem
associates.count_of_coprime
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_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) :
theorem
associates.count_mul_of_coprime
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a : associates α}
(ha : a ≠ 0)
{b : associates α}
(hb : b ≠ 0)
{p : associates α}
(hp : irreducible p)
(hab : ∀ (d : associates α), d ∣ a → d ∣ b → ¬prime d) :
theorem
associates.count_mul_of_coprime'
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a : associates α}
(ha : a ≠ 0)
{b : associates α}
(hb : b ≠ 0)
{p : associates α}
(hp : irreducible p)
(hab : ∀ (d : associates α), d ∣ a → d ∣ b → ¬prime d) :
theorem
associates.dvd_count_of_dvd_count_mul
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a b : associates α}
(ha : a ≠ 0)
(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) :
@[simp]
theorem
associates.factors_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)] :
@[simp]
theorem
associates.pow_factors
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a : associates α}
{k : ℕ} :
theorem
associates.count_pow
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a : associates α}
(ha : a ≠ 0)
{p : associates α}
(hp : irreducible p)
(k : ℕ) :
theorem
associates.dvd_count_pow
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{a : associates α}
(ha : a ≠ 0)
{p : associates α}
(hp : irreducible p)
(k : ℕ) :
theorem
associates.is_pow_of_dvd_count
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
{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_of_mul_eq_pow
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
[normalization_monoid α]
{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
def
unique_factorization_monoid.to_gcd_monoid
(α : Type u_1)
[integral_domain α]
[unique_factorization_monoid α]
[normalization_monoid α]
[decidable_eq (associates α)]
[decidable_eq α] :
to_gcd_monoid constructs a GCD monoid out of a normalization on a
unique factorization domain.
Equations
- unique_factorization_monoid.to_gcd_monoid α = {norm_unit := norm_unit _inst_3, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _, 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 := _, normalize_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}