mathlib3documentation

ring_theory.unique_factorization_domain

Unique factorization #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

To do #

• set up the complete lattice structure on factor_set.
@[class]
structure wf_dvd_monoid (α : Type u_2)  :
Prop
• 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
@[protected, instance]
@[protected, instance]
theorem wf_dvd_monoid.exists_irreducible_factor {α : Type u_1} {a : α} (ha : ¬) (ha0 : a 0) :
(i : α), i a
theorem wf_dvd_monoid.induction_on_irreducible {α : Type u_1} {P : α Prop} (a : α) (h0 : P 0) (hu : (u : α), P u) (hi : (a i : α), a 0 P a P (i * a)) :
P a
theorem wf_dvd_monoid.exists_factors {α : Type u_1} (a : α) :
a 0 ( (f : multiset α), ( (b : α), b f a)
theorem wf_dvd_monoid.not_unit_iff_exists_factors_eq {α : Type u_1} (a : α) (hn0 : a 0) :
¬ (f : multiset α), ( (b : α), b f f.prod = a f
@[class]
structure unique_factorization_monoid (α : Type u_2)  :
Prop
• to_wf_dvd_monoid :
• irreducible_iff_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
@[reducible]
theorem ufm_of_gcd_of_wf_dvd_monoid {α : Type u_1} [gcd_monoid α] :

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

@[protected, instance]
theorem unique_factorization_monoid.exists_prime_factors {α : Type u_1} (a : α) :
a 0 ( (f : multiset α), ( (b : α), b f prime b) a)
theorem unique_factorization_monoid.induction_on_prime {α : Type u_1} {P : α Prop} (a : α) (h₁ : P 0) (h₂ : (x : α), P x) (h₃ : (a p : α), a 0 P a P (p * a)) :
P a
theorem prime_factors_unique {α : Type u_1} {f g : multiset α} :
( (x : α), x f prime x) ( (x : α), x g prime x) g.prod
theorem unique_factorization_monoid.factors_unique {α : Type u_1} {f g : multiset α} (hf : (x : α), x f ) (hg : (x : α), x g ) (h : g.prod) :
theorem prime_factors_irreducible {α : Type u_1} {a : α} {f : multiset α} (ha : irreducible a) (pfa : ( (b : α), b f prime b) a) :
(p : α), 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} (pf : (a : α), a 0 ( (f : multiset α), ( (b : α), b f prime b) a)) :
theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} (pf : (a : α), a 0 ( (f : multiset α), ( (b : α), b f prime b) a)) {p : α} :
theorem unique_factorization_monoid.of_exists_prime_factors {α : Type u_1} (pf : (a : α), a 0 ( (f : multiset α), ( (b : α), b f prime b) a)) :
theorem unique_factorization_monoid.iff_exists_prime_factors {α : Type u_1}  :
(a : α), a 0 ( (f : multiset α), ( (b : α), b f prime b) a)
theorem mul_equiv.unique_factorization_monoid {α : Type u_1} {β : Type u_2} (e : α ≃* β) (hα : unique_factorization_monoid α) :
theorem mul_equiv.unique_factorization_monoid_iff {α : Type u_1} {β : Type u_2} (e : α ≃* β) :
theorem irreducible_iff_prime_of_exists_unique_irreducible_factors {α : Type u_1} (eif : (a : α), a 0 ( (f : multiset α), ( (b : α), b f a)) (uif : (f g : multiset α), ( (x : α), x f ( (x : α), x g g.prod ) (p : α) :
theorem unique_factorization_monoid.of_exists_unique_irreducible_factors {α : Type u_1} (eif : (a : α), a 0 ( (f : multiset α), ( (b : α), b f a)) (uif : (f g : multiset α), ( (x : α), x f ( (x : α), x g g.prod ) :
noncomputable def unique_factorization_monoid.factors {α : Type u_1} [decidable_eq α] (a : α) :

Noncomputably determines the multiset of prime factors.

Equations
• = dite (a = 0) (λ (h : a = 0), 0) (λ (h : ¬a = 0),
theorem unique_factorization_monoid.factors_prod {α : Type u_1} [decidable_eq α] {a : α} (ane0 : a 0) :
theorem unique_factorization_monoid.ne_zero_of_mem_factors {α : Type u_1} [decidable_eq α] {p a : α} (h : p ) :
a 0
theorem unique_factorization_monoid.dvd_of_mem_factors {α : Type u_1} [decidable_eq α] {p a : α} (h : p ) :
p a
theorem unique_factorization_monoid.prime_of_factor {α : Type u_1} [decidable_eq α] {a : α} (x : α) (hx : x ) :
theorem unique_factorization_monoid.irreducible_of_factor {α : Type u_1} [decidable_eq α] {a : α} (x : α) :
@[simp]
@[simp]
theorem unique_factorization_monoid.exists_mem_factors_of_dvd {α : Type u_1} [decidable_eq α] {a p : α} (ha0 : a 0) (hp : irreducible p) :
p a ( (q : α) (H : , q)
theorem unique_factorization_monoid.exists_mem_factors {α : Type u_1} [decidable_eq α] {x : α} (hx : x 0) (h : ¬) :
(p : α),
theorem unique_factorization_monoid.factors_mul {α : Type u_1} [decidable_eq α] {x y : α} (hx : x 0) (hy : y 0) :
theorem unique_factorization_monoid.factors_pow {α : Type u_1} [decidable_eq α] {x : α} (n : ) :
@[simp]
theorem unique_factorization_monoid.factors_pos {α : Type u_1} [decidable_eq α] (x : α) (hx : x 0) :
noncomputable def unique_factorization_monoid.normalized_factors {α : Type u_1} [decidable_eq α] (a : α) :

Noncomputably determines the multiset of prime factors.

Equations
@[simp]

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} [decidable_eq α] {a : α} (ane0 : a 0) :
theorem unique_factorization_monoid.normalized_factors_eq_of_dvd {α : Type u_1} [decidable_eq α] (a p : α) (q : α)  :
p q p = q
theorem unique_factorization_monoid.exists_mem_normalized_factors_of_dvd {α : Type u_1} [decidable_eq α] {a p : α} (ha0 : a 0) (hp : irreducible p) :
p a ( (q : α) (H : , q)
theorem unique_factorization_monoid.exists_mem_normalized_factors {α : Type u_1} [decidable_eq α] {x : α} (hx : x 0) (h : ¬) :
@[simp]
@[simp]
@[simp]
theorem unique_factorization_monoid.normalized_factors_mul {α : Type u_1} [decidable_eq α] {x y : α} (hx : x 0) (hy : y 0) :
@[simp]
theorem unique_factorization_monoid.normalized_factors_pow {α : Type u_1} [decidable_eq α] {x : α} (n : ) :
theorem irreducible.normalized_factors_pow {α : Type u_1} [decidable_eq α] {p : α} (hp : irreducible p) (k : ) :
theorem unique_factorization_monoid.normalized_factors_prod_eq {α : Type u_1} [decidable_eq α] (s : multiset α) (hs : (a : α), a s ) :
theorem unique_factorization_monoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} [decidable_eq α] {p r : α} (h : {m : α}, ) (hr : r 0) :
(i : ), associated (p ^ i) r
theorem unique_factorization_monoid.normalized_factors_prod_of_prime {α : Type u_1} [decidable_eq α] [nontrivial α] [unique αˣ] {m : multiset α} (h : (p : α), p m ) :
@[simp]
theorem unique_factorization_monoid.normalized_factors_pos {α : Type u_1} [decidable_eq α] (x : α) (hx : x 0) :
@[protected]
noncomputable def unique_factorization_monoid.normalization_monoid {α : Type u_1} [nontrivial α]  :

Noncomputably defines a normalization_monoid structure on a unique_factorization_monoid.

Equations
@[protected, instance]
Equations
theorem unique_factorization_monoid.no_factors_of_no_prime_factors {R : Type u_2} {a b : R} (ha : a 0) (h : {d : R}, d a d b ¬) {d : R} :
d a d b
theorem unique_factorization_monoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} {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.

theorem unique_factorization_monoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} {a b c : R} (ha : a 0) (no_factors : {d : R}, d a d b ¬) :
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} (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.

theorem unique_factorization_monoid.exists_reduced_factors' {R : Type u_2} (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
theorem unique_factorization_monoid.pow_right_injective {R : Type u_2} {a : R} (ha0 : a 0) (ha1 : ¬) :
theorem unique_factorization_monoid.pow_eq_pow_iff {R : Type u_2} {a : R} (ha0 : a 0) (ha1 : ¬) {i j : } :
a ^ i = a ^ j i = j

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} [nontrivial R] [decidable_eq R] {p x : R} (hp : irreducible p) (hnorm : = 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.

theorem unique_factorization_monoid.count_normalized_factors_eq' {R : Type u_2} [nontrivial R] [decidable_eq R] {p x : R} (hp : p = 0 ) (hnorm : = 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. This is a slightly more general version of unique_factorization_monoid.count_normalized_factors_eq that allows p = 0.

theorem unique_factorization_monoid.max_power_factor {R : Type u_2} [nontrivial R] {a₀ x : R} (h : a₀ 0) (hx : irreducible x) :
(n : ) (a : R), ¬x a a₀ = x ^ n * a
theorem unique_factorization_monoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [decidable_eq α] {s : finset α} (i : α ) (p : α) (hps : p s) (is_prime : (q : α), q ) (is_coprime : (q : α), q (q' : α), q' q q' q = q') (q : α) :
q p ^ i p q s.prod (λ (p' : α), p' ^ i p')
theorem unique_factorization_monoid.induction_on_prime_power {α : Type u_1} {P : α Prop} (s : finset α) (i : α ) (is_prime : (p : α), p s ) (is_coprime : (p : α), p s (q : α), q s p q p = q) (h1 : {x : α}, P x) (hpr : {p : α} (i : ), 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.

theorem unique_factorization_monoid.induction_on_coprime {α : Type u_1} {P : α Prop} (a : α) (h0 : P 0) (h1 : {x : α}, P x) (hpr : {p : α} (i : ), 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 : α.

theorem unique_factorization_monoid.multiplicative_prime_power {α : Type u_1} {β : Type u_3} {f : α β} (s : finset α) (i j : α ) (is_prime : (p : α), p s ) (is_coprime : (p : α), p s (q : α), q s p q p = q) (h1 : {x y : α}, f (x * y) = f x * f y) (hpr : {p : α} (i : ), 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.

theorem unique_factorization_monoid.multiplicative_of_coprime {α : Type u_1} {β : Type u_3} (f : α β) (a b : α) (h0 : f 0 = 0) (h1 : {x y : α}, f (x * y) = f x * f y) (hpr : {p : α} (i : ), 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.

@[reducible]
def associates.factor_set (α : 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
theorem associates.factor_set.coe_add {α : Type u_1} {a b : multiset {a // } :
(a + b) = a + b
def associates.factor_set.prod {α : Type u_1}  :

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

Equations
@[simp]
theorem associates.prod_top {α : Type u_1}  :
@[simp]
theorem associates.prod_coe {α : Type u_1} {s : multiset {a // } :
@[simp]
theorem associates.prod_add {α : Type u_1} (a b : associates.factor_set α) :
(a + b).prod = a.prod * b.prod
theorem associates.prod_mono {α : Type u_1} {a b : associates.factor_set α} :
a b a.prod b.prod
def associates.bcount {α : Type u_1} [decidable_eq (associates α)] (p : {a // ) :

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

Equations
def associates.count {α : Type u_1} [dec_irr : Π (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
@[simp]
theorem associates.count_some {α : Type u_1} [dec_irr : Π (p : , ] [decidable_eq (associates α)] {p : associates α} (hp : irreducible p) (s : multiset {a // ) :
@[simp]
theorem associates.count_zero {α : Type u_1} [dec_irr : Π (p : , ] [decidable_eq (associates α)] {p : associates α} (hp : irreducible p) :
p.count 0 = 0
theorem associates.count_reducible {α : Type u_1} [dec_irr : Π (p : , ] [decidable_eq (associates α)] {p : associates α} (hp : ¬) :
p.count = 0
def associates.bfactor_set_mem {α : Type u_1}  :
{a // Prop

membership in a factor_set (bundled version)

Equations
def associates.factor_set_mem {α : Type u_1} [dec_irr : Π (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
@[protected, instance]
def associates.factor_set.has_mem {α : Type u_1} [dec_irr : Π (p : , ] :
Equations
@[simp]
theorem associates.factor_set_mem_eq_mem {α : Type u_1} [dec_irr : Π (p : , ] (p : associates α) (s : associates.factor_set α) :
= (p s)
theorem associates.mem_factor_set_top {α : Type u_1} [dec_irr : Π (p : , ] {p : associates α} {hp : irreducible p} :
theorem associates.mem_factor_set_some {α : Type u_1} [dec_irr : Π (p : , ] {p : associates α} {hp : irreducible p} {l : multiset {a // } :
p l p, hp⟩ l
theorem associates.reducible_not_mem_factor_set {α : Type u_1} [dec_irr : Π (p : , ] {p : associates α} (hp : ¬) (s : associates.factor_set α) :
p s
theorem associates.unique' {α : Type u_1} {p q : multiset (associates α)} :
( (a : , a p ( (a : , a q p.prod = q.prod p = q
theorem associates.factor_set.unique {α : Type u_1} [nontrivial α] {p q : associates.factor_set α} (h : p.prod = q.prod) :
p = q
theorem associates.prod_le_prod_iff_le {α : Type u_1} [nontrivial α] {p q : multiset (associates α)} (hp : (a : , a p ) (hq : (a : , a q ) :
p.prod q.prod p q
noncomputable def associates.factors' {α : Type u_1} [dec : decidable_eq α] (a : α) :
multiset {a //

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

Equations
@[simp]
theorem associates.map_subtype_coe_factors' {α : Type u_1} [dec : decidable_eq α] {a : α} :
theorem associates.factors'_cong {α : Type u_1} [dec : decidable_eq α] {a b : α} (h : b) :
noncomputable def associates.factors {α : Type u_1} [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.

Equations
@[simp]
theorem associates.factors_0 {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :
@[simp]
theorem associates.factors_mk {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a : α) (h : a 0) :
@[simp]
theorem associates.factors_prod {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a : associates α) :
theorem associates.prod_factors {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] (s : associates.factor_set α) :
theorem associates.factors_subsingleton {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [subsingleton α] {a : associates α} :
theorem associates.factors_eq_none_iff_zero {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} :
a = 0
theorem associates.factors_eq_some_iff_ne_zero {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} :
( (s : multiset {p // irreducible p}), a.factors = a 0
theorem associates.eq_of_factors_eq_factors {α : Type u_1} [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} [nontrivial α] {a b : associates.factor_set α} (h : a.prod = b.prod) :
a = b
theorem associates.eq_factors_of_eq_counts {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (ha : a 0) (hb : b 0) (h : (p : , p.count a.factors = p.count b.factors) :
theorem associates.eq_of_eq_counts {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (ha : a 0) (hb : b 0) (h : (p : , p.count a.factors = p.count b.factors) :
a = b
theorem associates.count_le_count_of_factors_le {α : Type u_1} [dec_irr : Π (p : , ] [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} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a b : associates α) :
theorem associates.factors_mono {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} :
theorem associates.factors_le {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} :
theorem associates.count_le_count_of_le {α : Type u_1} [dec_irr : Π (p : , ] [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} [nontrivial α] {a b : associates.factor_set α} :
a.prod b.prod a b
@[protected, instance]
noncomputable def associates.has_sup {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :
Equations
@[protected, instance]
noncomputable def associates.has_inf {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :
Equations
@[protected, instance]
noncomputable def associates.lattice {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] :
Equations
theorem associates.sup_mul_inf {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a b : associates α) :
(a b) * (a b) = a * b
theorem associates.dvd_of_mem_factors {α : Type u_1} [dec_irr : Π (p : , ] [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} [dec_irr : Π (p : , ] [dec : decidable_eq α] {a : α} {p : associates α} {hp : irreducible p} {hz : a 0} (h_mem : p, hp⟩ ) :
theorem associates.mem_factors'_of_dvd {α : Type u_1} [dec : decidable_eq α] {a p : α} (ha0 : a 0) (hp : irreducible p) (hd : p a) :
theorem associates.mem_factors'_iff_dvd {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] {a p : α} (ha0 : a 0) (hp : irreducible p) :
p a
theorem associates.mem_factors_of_dvd {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} (ha0 : a 0) (hp : irreducible p) (hd : p a) :
theorem associates.mem_factors_iff_dvd {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} (ha0 : a 0) (hp : irreducible p) :
p a
theorem associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : α} (ha : a 0) (hb : b 0) (h : 1) :
(p : α), p a p b
theorem associates.coprime_iff_inf_one {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : α} (ha0 : a 0) (hb0 : b 0) :
= 1 {d : α}, d a d b ¬
theorem associates.factors_self {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {p : associates α} (hp : irreducible p) :
p.factors = option.some {p, hp⟩}
theorem associates.factors_prime_pow {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {p : associates α} (hp : irreducible p) (k : ) :
(p ^ k).factors = option.some p, hp⟩)
theorem associates.prime_pow_dvd_iff_le {α : Type u_1} [dec_irr : Π (p : , ] [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
theorem associates.le_of_count_ne_zero {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {m p : associates α} (h0 : m 0) (hp : irreducible p) :
p.count m.factors 0 p m
theorem associates.count_ne_zero_iff_dvd {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} (ha0 : a 0) (hp : irreducible p) :
theorem associates.count_self {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {p : associates α} (hp : irreducible p) :
theorem associates.count_eq_zero_of_ne {α : Type u_1} [dec_irr : Π (p : , ] [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} [dec_irr : Π (p : , ] [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} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {b : associates α} (hb : b 0) (hab : (d : , d a d b ¬) {p : associates α} (hp : irreducible p) :
theorem associates.count_mul_of_coprime {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (hb : b 0) {p : associates α} (hp : irreducible p) (hab : (d : , d a d b ¬) :
theorem associates.count_mul_of_coprime' {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b p : associates α} (hp : irreducible p) (hab : (d : , d a d b ¬) :
theorem associates.dvd_count_of_dvd_count_mul {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (hb : b 0) {p : associates α} (hp : irreducible p) (hab : (d : , d a d b ¬) {k : } (habk : k p.count (a * b).factors) :
@[simp]
theorem associates.factors_one {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] :
@[simp]
theorem associates.pow_factors {α : Type u_1} [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {a : associates α} {k : } :
(a ^ k).factors = k a.factors
theorem associates.count_pow {α : Type u_1} [dec_irr : Π (p : , ] [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
theorem associates.dvd_count_pow {α : Type u_1} [dec_irr : Π (p : , ] [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
theorem associates.is_pow_of_dvd_count {α : Type u_1} [dec_irr : Π (p : , ] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] [nontrivial α] {a : associates α} (ha : a 0) {k : } (hk : (p : , k p.count a.factors) :
(b : , a = b ^ k
theorem associates.eq_pow_count_factors_of_dvd_pow {α : Type u_1} [dec_irr : Π (p : , ] [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).

theorem associates.count_factors_eq_find_of_dvd_pow {α : Type u_1} [dec_irr : Π (p : , ] [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} [nontrivial α] {a b c : associates α} (ha : a 0) (hb : b 0) (hab : (d : , d a d b ¬) {k : } (h : a * b = c ^ k) :
(d : , a = d ^ k
theorem associates.eq_pow_find_of_dvd_irreducible_pow {α : Type u_1} {a p : associates α} (hp : irreducible p) [Π (n : ), decidable (a p ^ n)] {n : } (h : a p ^ n) :
a = p ^

The only divisors of prime powers are prime powers.

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

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

Equations

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

Equations
noncomputable def unique_factorization_monoid.fintype_subtype_dvd {M : Type u_1} [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
noncomputable def factorization {α : Type u_1} [decidable_eq α] (n : α) :

This returns the multiset of irreducible factors as a finsupp

Equations
theorem factorization_eq_count {α : Type u_1} [decidable_eq α] {n p : α} :
@[simp]
theorem factorization_zero {α : Type u_1} [decidable_eq α] :
@[simp]
theorem factorization_one {α : Type u_1} [decidable_eq α] :
@[simp]
theorem support_factorization {α : Type u_1} [decidable_eq α] {n : α} :

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

@[simp]
theorem factorization_mul {α : Type u_1} [decidable_eq α] {a b : α} (ha : a 0) (hb : b 0) :

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} [decidable_eq α] {x : α} {n : } :

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} [decidable_eq α] (a b : α) (ha : a 0) (hb : b 0) (h : = ) :
b