Unique factorization #
Main Definitions #
wf_dvd_monoidholds formonoids for which a strict divisibility relation is well-founded.unique_factorization_monoidholds forwf_dvd_monoids whereirreducibleis equivalent toprime
To do #
- set up the complete lattice structure on
factor_set.
@[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.
@[protected, instance]
def
is_noetherian_ring.wf_dvd_monoid
{α : Type u_1}
[comm_ring α]
[is_domain α]
[is_noetherian_ring α] :
theorem
wf_dvd_monoid.of_wf_dvd_monoid_associates
{α : Type u_1}
[comm_monoid_with_zero α]
(h : wf_dvd_monoid (associates α)) :
@[protected, 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 ≠ 0 → (∃ (f : multiset α), (∀ (b : α), b ∈ f → irreducible b) ∧ associated f.prod a)
theorem
wf_dvd_monoid.of_well_founded_associates
{α : Type u_1}
[cancel_comm_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 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
theorem
ufm_of_gcd_of_wf_dvd_monoid
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[wf_dvd_monoid α]
[gcd_monoid α] :
Can't be an instance because it would cause a loop ufm → wf_dvd_monoid → ufm → ....
@[protected, instance]
def
associates.ufm
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α] :
theorem
unique_factorization_monoid.exists_prime_factors
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
(a : α) :
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
theorem
unique_factorization_monoid.factors_unique
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
{f g : multiset α} :
(∀ (x : α), x ∈ f → irreducible x) → (∀ (x : α), x ∈ g → irreducible x) → associated f.prod g.prod → multiset.rel associated f g
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
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.
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)) :
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
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)) :
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)
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 α) :
theorem
mul_equiv.unique_factorization_monoid_iff
{α : Type u_1}
{β : Type u_2}
[cancel_comm_monoid_with_zero α]
[cancel_comm_monoid_with_zero β]
(e : α ≃* β) :
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
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) :
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 _)
theorem
unique_factorization_monoid.factors_prod
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq α]
[unique_factorization_monoid α]
{a : α}
(ane0 : a ≠ 0) :
theorem
unique_factorization_monoid.prime_of_factor
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq α]
[unique_factorization_monoid α]
{a : α}
(x : α) :
theorem
unique_factorization_monoid.irreducible_of_factor
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq α]
[unique_factorization_monoid α]
{a : α}
(x : α) :
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)
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.
@[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) :
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
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) :
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 : α) :
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 : α) :
theorem
unique_factorization_monoid.normalize_normalized_factor
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq α]
[normalization_monoid α]
[unique_factorization_monoid α]
{a : α}
(x : α) :
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) :
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)
@[simp]
theorem
unique_factorization_monoid.normalized_factors_zero
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq α]
[normalization_monoid α]
[unique_factorization_monoid α] :
@[simp]
theorem
unique_factorization_monoid.normalized_factors_one
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq α]
[normalization_monoid α]
[unique_factorization_monoid α] :
@[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) :
@[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 : ℕ) :
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 : ℕ) :
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) :
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 : ℕ) :
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 : α) :
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
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
@[protected]
noncomputable
def
unique_factorization_monoid.normalization_monoid
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[nontrivial α]
[unique_factorization_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
@[protected, instance]
noncomputable
def
unique_factorization_monoid.normalization_monoid.inhabited
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[nontrivial α]
[unique_factorization_monoid α] :
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} :
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) :
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_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) :
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}
[cancel_comm_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}
[cancel_comm_monoid_with_zero R]
[unique_factorization_monoid R]
(a b : R)
(hb : b ≠ 0) :
theorem
unique_factorization_monoid.le_multiplicity_iff_repeat_le_normalized_factors
{R : Type u_2}
[cancel_comm_monoid_with_zero R]
[unique_factorization_monoid R]
[nontrivial R]
[normalization_monoid R]
[decidable_eq R]
[dec_dvd : decidable_rel has_dvd.dvd]
{a b : R}
{n : ℕ}
(ha : irreducible a)
(hb : b ≠ 0) :
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]
[decidable_eq R]
[dec_dvd : decidable_rel has_dvd.dvd]
{a b : R}
(ha : irreducible a)
(hb : b ≠ 0) :
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 _) _..
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) :
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.
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})
theorem
associates.factor_set.coe_add
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
{a b : multiset {a // irreducible a}} :
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 α) :
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}
[cancel_comm_monoid_with_zero α]
{s : multiset {a // irreducible a}} :
@[simp]
theorem
associates.prod_add
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
(a b : associates.factor_set α) :
theorem
associates.prod_mono
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
{a b : associates.factor_set α} :
theorem
associates.factor_set.prod_eq_zero_iff
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[nontrivial α]
(p : associates.factor_set α) :
def
associates.bcount
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[decidable_eq (associates α)]
(p : {a // irreducible a}) :
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}
[cancel_comm_monoid_with_zero α]
[dec_irr : Π (p : associates α), decidable (irreducible p)]
[decidable_eq (associates α)]
(p : associates α) :
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}
[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 (some s) = multiset.count ⟨p, hp⟩ s
@[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) :
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) :
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 (some l) = (p ∈ l)
- associates.bfactor_set_mem _x ⊤ = true
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)
@[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)}
@[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)
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} :
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}} :
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
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
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
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) :
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) _
@[simp]
theorem
associates.map_subtype_coe_factors'
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[dec : decidable_eq α]
{a : α} :
theorem
associates.factors'_cong
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[dec : decidable_eq α]
{a b : α}
(h : associated a b) :
noncomputable
def
associates.factors
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_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}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)] :
@[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)
@[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 α) :
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 α) :
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 α} :
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 α} :
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 α} :
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
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
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) :
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
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) :
@[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 α) :
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 α} :
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 α} :
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) :
theorem
associates.prod_le
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[nontrivial α]
{a b : associates.factor_set α} :
@[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}
@[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}
@[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 := _}
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 α) :
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
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
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
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
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
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
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) :
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
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) :
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 : ℕ) :
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 : ℕ} :
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) :
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
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[simp]
theorem
associates.factors_one
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[dec : decidable_eq α]
[dec' : decidable_eq (associates α)]
[nontrivial α] :
@[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 : ℕ} :
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 : ℕ) :
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 : ℕ) :
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
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) :
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}
[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) :
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
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) :
The only divisors of prime powers are prime powers.
theorem
associates.quot_out
{α : Type u_1}
[comm_monoid α]
(a : associates α) :
associates.mk (quot.out a) = a
noncomputable
def
unique_factorization_monoid.to_gcd_monoid
(α : Type u_1)
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[decidable_eq (associates α)]
[decidable_eq α] :
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 := _}
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 α] :
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 := 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 := _}
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) :
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.product finset.univ)) _
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
theorem
factorization_eq_count
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[normalization_monoid α]
[decidable_eq α]
{n p : α} :
@[simp]
theorem
factorization_zero
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[normalization_monoid α]
[decidable_eq α] :
factorization 0 = 0
@[simp]
theorem
factorization_one
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[normalization_monoid α]
[decidable_eq α] :
factorization 1 = 0
@[simp]
theorem
support_factorization
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
[unique_factorization_monoid α]
[normalization_monoid α]
[decidable_eq α]
{n : α} :
The support of factorization n is exactly the finset of normalized factors
@[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
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
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