# Unique factorization #

## Main Definitions #

• WfDvdMonoid holds for Monoids for which a strict divisibility relation is well-founded.
• UniqueFactorizationMonoid holds for WfDvdMonoids where Irreducible is equivalent to Prime

## To do #

• set up the complete lattice structure on FactorSet.
class WfDvdMonoid (α : Type u_2) :

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
theorem WfDvdMonoid.wellFounded_dvdNotUnit {α : Type u_2} [self : ] :
WellFounded DvdNotUnit
@[instance 100]
instance IsNoetherianRing.wfDvdMonoid {α : Type u_1} [] [] [] :
Equations
• =
instance WfDvdMonoid.wfDvdMonoid_associates {α : Type u_1} [] :
Equations
• =
theorem WfDvdMonoid.wellFounded_associates {α : Type u_1} [] :
WellFounded fun (x x_1 : ) => x < x_1
theorem WfDvdMonoid.exists_irreducible_factor {α : Type u_1} [] {a : α} (ha : ¬) (ha0 : a 0) :
∃ (i : α), i a
theorem WfDvdMonoid.induction_on_irreducible {α : Type u_1} [] {P : αProp} (a : α) (h0 : P 0) (hu : ∀ (u : α), P u) (hi : ∀ (a i : α), a 0P aP (i * a)) :
P a
theorem WfDvdMonoid.exists_factors {α : Type u_1} [] (a : α) :
a 0∃ (f : ), (bf, ) Associated f.prod a
theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [] (a : α) (hn0 : a 0) :
¬ ∃ (f : ), (bf, ) f.prod = a f
theorem WfDvdMonoid.isRelPrime_of_no_irreducible_factors {α : Type u_1} [] {x : α} {y : α} (nonzero : ¬(x = 0 y = 0)) (H : ∀ (z : α), z x¬z y) :
theorem WfDvdMonoid.of_wellFounded_associates {α : Type u_1} (h : WellFounded fun (x x_1 : ) => x < x_1) :
theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} :
WellFounded fun (x x_1 : ) => x < x_1
theorem WfDvdMonoid.max_power_factor' {α : Type u_1} [] {a₀ : α} {x : α} (h : a₀ 0) (hx : ¬) :
∃ (n : ) (a : α), ¬x a a₀ = x ^ n * a
theorem WfDvdMonoid.max_power_factor {α : Type u_1} [] {a₀ : α} {x : α} (h : a₀ 0) (hx : ) :
∃ (n : ) (a : α), ¬x a a₀ = x ^ n * a
theorem multiplicity.finite_of_not_isUnit {α : Type u_1} [] {a : α} {b : α} (ha : ¬) (hb : b 0) :
class UniqueFactorizationMonoid (α : Type u_2) extends :

unique factorization monoids.

These are defined as CancelCommMonoidWithZeros with well-founded strict divisibility relations, but this is equivalent to more familiar definitions:

Each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements.

Each element (except zero) is non-uniquely represented as a multiset of prime factors.

To define a UFD using the definition in terms of multisets of irreducible factors, use the definition of_exists_unique_irreducible_factors

To define a UFD using the definition in terms of multisets of prime factors, use the definition of_exists_prime_factors

• wellFounded_dvdNotUnit : WellFounded DvdNotUnit
• irreducible_iff_prime : ∀ {a : α},
Instances
theorem UniqueFactorizationMonoid.irreducible_iff_prime {α : Type u_2} [self : ] {a : α} :

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

@[deprecated ufm_of_decomposition_of_wfDvdMonoid]
theorem ufm_of_gcd_of_wfDvdMonoid {α : Type u_1} [] :

Alias of ufm_of_decomposition_of_wfDvdMonoid.

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

instance Associates.ufm {α : Type u_1} :
Equations
• =
theorem UniqueFactorizationMonoid.exists_prime_factors {α : Type u_1} (a : α) :
a 0∃ (f : ), (bf, ) Associated f.prod a
Equations
• =
theorem UniqueFactorizationMonoid.exists_prime_iff {α : Type u_1} :
(∃ (p : α), ) ∃ (x : α), x 0 ¬
theorem UniqueFactorizationMonoid.induction_on_prime {α : Type u_1} {P : αProp} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), P x) (h₃ : ∀ (a p : α), a 0P aP (p * a)) :
P a
theorem prime_factors_unique {α : Type u_1} {f : } {g : } :
(xf, )(xg, )Associated f.prod g.prodMultiset.Rel Associated f g
theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} {f : } {g : } (hf : xf, ) (hg : xg, ) (h : Associated f.prod g.prod) :
Multiset.Rel Associated f g
theorem prime_factors_irreducible {α : Type u_1} {a : α} {f : } (ha : ) (pfa : (bf, ) Associated f.prod a) :
∃ (p : α), f = {p}

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

theorem WfDvdMonoid.of_exists_prime_factors {α : Type u_1} (pf : ∀ (a : α), a 0∃ (f : ), (bf, ) Associated f.prod a) :
theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} (pf : ∀ (a : α), a 0∃ (f : ), (bf, ) Associated f.prod a) {p : α} :
theorem UniqueFactorizationMonoid.of_exists_prime_factors {α : Type u_1} (pf : ∀ (a : α), a 0∃ (f : ), (bf, ) Associated f.prod a) :
theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} :
∀ (a : α), a 0∃ (f : ), (bf, ) Associated f.prod a
theorem MulEquiv.uniqueFactorizationMonoid {α : Type u_1} {β : Type u_2} (e : α ≃* β) (hα : ) :
theorem MulEquiv.uniqueFactorizationMonoid_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 : ), (bf, ) Associated f.prod a) (uif : ∀ (f g : ), (xf, )(xg, )Associated f.prod g.prodMultiset.Rel Associated f g) (p : α) :
theorem UniqueFactorizationMonoid.of_exists_unique_irreducible_factors {α : Type u_1} (eif : ∀ (a : α), a 0∃ (f : ), (bf, ) Associated f.prod a) (uif : ∀ (f g : ), (xf, )(xg, )Associated f.prod g.prodMultiset.Rel Associated f g) :
noncomputable def UniqueFactorizationMonoid.factors {α : Type u_1} (a : α) :

Noncomputably determines the multiset of prime factors.

Equations
• = if h : a = 0 then 0 else
Instances For
theorem UniqueFactorizationMonoid.factors_prod {α : Type u_1} {a : α} (ane0 : a 0) :
@[simp]
theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors {α : Type u_1} {p : α} {a : α} (h : ) :
a 0
theorem UniqueFactorizationMonoid.dvd_of_mem_factors {α : Type u_1} {p : α} {a : α} (h : ) :
p a
theorem UniqueFactorizationMonoid.prime_of_factor {α : Type u_1} {a : α} (x : α) (hx : ) :
theorem UniqueFactorizationMonoid.irreducible_of_factor {α : Type u_1} {a : α} (x : α) :
theorem UniqueFactorizationMonoid.exists_mem_factors_of_dvd {α : Type u_1} {a : α} {p : α} (ha0 : a 0) (hp : ) :
p a
theorem UniqueFactorizationMonoid.exists_mem_factors {α : Type u_1} {x : α} (hx : x 0) (h : ¬) :
∃ (p : α),
theorem UniqueFactorizationMonoid.factors_mul {α : Type u_1} {x : α} {y : α} (hx : x 0) (hy : y 0) :
theorem UniqueFactorizationMonoid.factors_pow {α : Type u_1} {x : α} (n : ) :
Multiset.Rel Associated ()
@[simp]
theorem UniqueFactorizationMonoid.factors_pos {α : Type u_1} (x : α) (hx : x 0) :
theorem UniqueFactorizationMonoid.factors_pow_count_prod {α : Type u_1} [] {x : α} (hx : x 0) :
Associated (.toFinset.prod fun (p : α) => ) x
noncomputable def UniqueFactorizationMonoid.normalizedFactors {α : Type u_1} (a : α) :

Noncomputably determines the multiset of prime factors.

Equations
Instances For
@[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 UniqueFactorizationMonoid.normalizedFactors_prod {α : Type u_1} {a : α} (ane0 : a 0) :
theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} {a : α} (x : α) :
normalize x = x
theorem UniqueFactorizationMonoid.normalizedFactors_irreducible {α : Type u_1} {a : α} (ha : ) :
= {normalize a}
theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} (a : α) (p : α) :
q, p qp = q
theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd {α : Type u_1} {a : α} {p : α} (ha0 : a 0) (hp : ) :
p a
theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors {α : Type u_1} {x : α} (hx : x 0) (h : ¬) :
∃ (p : α),
@[simp]
@[simp]
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_mul {α : Type u_1} {x : α} {y : α} (hx : x 0) (hy : y 0) :
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_pow {α : Type u_1} {x : α} (n : ) :
theorem Irreducible.normalizedFactors_pow {α : Type u_1} {p : α} (hp : ) (k : ) :
= Multiset.replicate k (normalize p)
theorem UniqueFactorizationMonoid.normalizedFactors_prod_eq {α : Type u_1} (s : ) (hs : as, ) :
= Multiset.map (normalize) s
theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors {α : Type u_1} {x : α} {y : α} (hx : x 0) (hy : y 0) :
theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors {α : Type u_1} {x : α} {y : α} (hx : x 0) (hy : y 0) :
theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow {α : Type u_1} {p : α} (hp : ) (k : ) :
= Multiset.replicate k (normalize p)
theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff {α : Type u_1} [] {p : α} {x : α} (hx : x 0) :
p x
theorem UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} {p : α} {r : α} (h : ∀ {m : α}, ) (hr : r 0) :
∃ (i : ), Associated (p ^ i) r
theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime {α : Type u_1} [] [] {m : } (h : pm, ) :
theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated {α : Type u_1} {a : α} {b : α} {c : α} (ha : ) (hb : ) (h : ) :
a = b
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_pos {α : Type u_1} (x : α) (hx : x 0) :
theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {α : Type u_1} {x : α} {y : α} (hx : x 0) (hy : y 0) :
theorem UniqueFactorizationMonoid.normalizedFactors_multiset_prod {α : Type u_1} (s : ) (hs : 0s) :
= (Multiset.map UniqueFactorizationMonoid.normalizedFactors s).sum

Noncomputably defines a normalizationMonoid structure on a UniqueFactorizationMonoid.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors {R : Type u_2} {a : R} {b : R} (ha : a 0) :
∀ ⦃d : R⦄, d ad b¬
theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} {a : R} {b : R} {c : R} (ha : a 0) (h : ∀ ⦃d : R⦄, d ad c¬) :
a b * ca b

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

theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} {a : R} {b : R} {c : R} (ha : a 0) (no_factors : ∀ {d : R}, d ad b¬) :
a b * ca c

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

theorem UniqueFactorizationMonoid.exists_reduced_factors {R : Type u_2} (a : R) :
a 0∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' c' * a' = a c' * b' = b

If a ≠ 0, b are elements of a unique factorization domain, then dividing out their common factor c' gives a' and b' with no factors in common.

theorem UniqueFactorizationMonoid.exists_reduced_factors' {R : Type u_2} (a : R) (b : R) (hb : b 0) :
∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' c' * a' = a c' * b' = b
theorem UniqueFactorizationMonoid.pow_right_injective {R : Type u_2} {a : R} (ha0 : a 0) (ha1 : ¬) :
Function.Injective fun (x : ) => a ^ x
theorem UniqueFactorizationMonoid.pow_eq_pow_iff {R : Type u_2} {a : R} (ha0 : a 0) (ha1 : ¬) {i : } {j : } :
a ^ i = a ^ j i = j
theorem UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors {R : Type u_2} [DecidableRel Dvd.dvd] {a : R} {b : R} {n : } (ha : ) (hb : b 0) :
n Multiset.replicate n (normalize a)
theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors {R : Type u_2} [DecidableRel Dvd.dvd] [] {a : R} {b : R} (ha : ) (hb : b 0) :
= (Multiset.count (normalize a) )

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

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

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq {R : Type u_2} [] {p : R} {x : R} (hp : ) (hnorm : normalize p = p) {n : } (hle : p ^ n x) (hlt : ¬p ^ (n + 1) x) :

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

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

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq' {R : Type u_2} [] {p : R} {x : R} (hp : p = 0 ) (hnorm : normalize p = p) {n : } (hle : p ^ n x) (hlt : ¬p ^ (n + 1) x) :

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

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

@[deprecated WfDvdMonoid.max_power_factor]
theorem UniqueFactorizationMonoid.max_power_factor {R : Type u_2} {a₀ : R} {x : R} (h : a₀ 0) (hx : ) :
∃ (n : ) (a : R), ¬x a a₀ = x ^ n * a

Deprecated. Use WfDvdMonoid.max_power_factor instead.

theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [] {s : } (i : α) (p : α) (hps : ps) (is_prime : qinsert p s, ) (is_coprime : qinsert p s, q'insert p s, q q'q = q') :
IsRelPrime (p ^ i p) (s.prod fun (p' : α) => p' ^ i p')
theorem UniqueFactorizationMonoid.induction_on_prime_power {α : Type u_1} {P : αProp} (s : ) (i : α) (is_prime : ps, ) (is_coprime : ps, qs, p qp = q) (h1 : ∀ {x : α}, P x) (hpr : ∀ {p : α} (i : ), P (p ^ i)) (hcp : ∀ {x y : α}, P xP yP (x * y)) :
P (s.prod fun (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 UniqueFactorizationMonoid.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 xP yP (x * y)) :
P a

If P holds for 0, units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on all a : α.

theorem UniqueFactorizationMonoid.multiplicative_prime_power {α : Type u_1} {β : Type u_3} {f : αβ} (s : ) (i : α) (j : α) (is_prime : ps, ) (is_coprime : ps, qs, p qp = q) (h1 : ∀ {x y : α}, f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ), f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, f (x * y) = f x * f y) :
f (s.prod fun (p : α) => p ^ (i p + j p)) = f (s.prod fun (p : α) => p ^ i p) * f (s.prod fun (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 UniqueFactorizationMonoid.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 : α}, f (x * y) = f x * f y) :
f (a * b) = f a * f b

If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative everywhere.

@[reducible, inline]
abbrev Associates.FactorSet (α : Type u) :

FactorSet α representation elements of unique factorization domain as multisets. Multiset α produced by normalizedFactors are only unique up to associated elements, while the multisets in FactorSet α are unique by equality and restricted to irreducible elements. This gives us a representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete lattice structure. Infimum is the greatest common divisor and supremum is the least common multiple.

Equations
Instances For
theorem Associates.FactorSet.coe_add {α : Type u_1} {a : Multiset { a : // }} {b : Multiset { a : // }} :
(a + b) = a + b
theorem Associates.FactorSet.sup_add_inf_eq_add {α : Type u_1} [] (a : ) (b : ) :
a b + a b = a + b

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

Equations
Instances For
@[simp]
theorem Associates.prod_top {α : Type u_1} :
.prod = 0
@[simp]
theorem Associates.prod_coe {α : Type u_1} {s : Multiset { a : // }} :
= (Multiset.map Subtype.val s).prod
@[simp]
theorem Associates.prod_add {α : Type u_1} (a : ) (b : ) :
(a + b).prod = a.prod * b.prod
theorem Associates.prod_mono {α : Type u_1} {a : } {b : } :
a ba.prod b.prod
theorem Associates.FactorSet.prod_eq_zero_iff {α : Type u_1} [] (p : ) :
p.prod = 0 p =
def Associates.bcount {α : Type u_1} [] (p : { a : // }) :

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

Equations
• = match x with | none => 0 | some s =>
Instances For
def Associates.count {α : Type u_1} [] [(p : ) → ] (p : ) :

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

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

Equations
Instances For
@[simp]
theorem Associates.count_some {α : Type u_1} [] [(p : ) → ] {p : } (hp : ) (s : Multiset { a : // }) :
p.count s = Multiset.count p, hp s
@[simp]
theorem Associates.count_zero {α : Type u_1} [] [(p : ) → ] {p : } (hp : ) :
p.count 0 = 0
theorem Associates.count_reducible {α : Type u_1} [] [(p : ) → ] {p : } (hp : ) :
p.count = 0
def Associates.BfactorSetMem {α : Type u_1} :
{ a : // }

membership in a FactorSet (bundled version)

Equations
• = match x✝, x with | x, none => True | p, some l => p l
Instances For
def Associates.FactorSetMem {α : Type u_1} (p : ) (s : ) :

FactorSetMem p s is the predicate that the irreducible p is a member of s : FactorSet α.

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

Equations
Instances For
Equations
• Associates.instMembershipFactorSet = { mem := Associates.FactorSetMem }
@[simp]
theorem Associates.factorSetMem_eq_mem {α : Type u_1} (p : ) (s : ) :
p.FactorSetMem s = (p s)
theorem Associates.mem_factorSet_top {α : Type u_1} {p : } {hp : } :
theorem Associates.mem_factorSet_some {α : Type u_1} {p : } {hp : } {l : Multiset { a : // }} :
p l p, hp l
theorem Associates.reducible_not_mem_factorSet {α : Type u_1} {p : } (hp : ) (s : ) :
ps
theorem Associates.irreducible_of_mem_factorSet {α : Type u_1} {p : } {s : } (h : p s) :
theorem Associates.unique' {α : Type u_1} {p : } {q : } :
(ap, )(aq, )p.prod = q.prodp = q
theorem Associates.FactorSet.unique {α : Type u_1} [] {p : } {q : } (h : p.prod = q.prod) :
p = q
theorem Associates.prod_le_prod_iff_le {α : Type u_1} [] {p : } {q : } (hp : ap, ) (hq : aq, ) :
p.prod q.prod p q
noncomputable def Associates.factors' {α : Type u_1} (a : α) :
Multiset { a : // }

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

Equations
Instances For
@[simp]
theorem Associates.map_subtype_coe_factors' {α : Type u_1} {a : α} :
Multiset.map Subtype.val = Multiset.map Associates.mk
theorem Associates.factors'_cong {α : Type u_1} {a : α} {b : α} (h : ) :
noncomputable def Associates.factors {α : Type u_1} (a : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Associates.factors_zero {α : Type u_1} :
@[deprecated Associates.factors_zero]
theorem Associates.factors_0 {α : Type u_1} :

Alias of Associates.factors_zero.

@[simp]
theorem Associates.factors_mk {α : Type u_1} (a : α) (h : a 0) :
().factors =
@[simp]
theorem Associates.factors_prod {α : Type u_1} (a : ) :
a.factors.prod = a
@[simp]
theorem Associates.prod_factors {α : Type u_1} [] (s : ) :
s.prod.factors = s
theorem Associates.factors_subsingleton {α : Type u_1} [] {a : } :
a.factors =
theorem Associates.factors_eq_top_iff_zero {α : Type u_1} {a : } :
a.factors = a = 0
@[deprecated Associates.factors_eq_top_iff_zero]
theorem Associates.factors_eq_none_iff_zero {α : Type u_1} {a : } :
a.factors = a = 0

Alias of Associates.factors_eq_top_iff_zero.

theorem Associates.factors_eq_some_iff_ne_zero {α : Type u_1} {a : } :
(∃ (s : Multiset { p : // }), a.factors = s) a 0
theorem Associates.eq_of_factors_eq_factors {α : Type u_1} {a : } {b : } (h : a.factors = b.factors) :
a = b
theorem Associates.eq_of_prod_eq_prod {α : Type u_1} [] {a : } {b : } (h : a.prod = b.prod) :
a = b
@[simp]
theorem Associates.factors_mul {α : Type u_1} (a : ) (b : ) :
(a * b).factors = a.factors + b.factors
theorem Associates.factors_mono {α : Type u_1} {a : } {b : } :
a ba.factors b.factors
@[simp]
theorem Associates.factors_le {α : Type u_1} {a : } {b : } :
a.factors b.factors a b
theorem Associates.eq_factors_of_eq_counts {α : Type u_1} [] [(p : ) → ] {a : } {b : } (ha : a 0) (hb : b 0) (h : ∀ (p : ), p.count a.factors = p.count b.factors) :
a.factors = b.factors
theorem Associates.eq_of_eq_counts {α : Type u_1} [] [(p : ) → ] {a : } {b : } (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} [] [(p : ) → ] {a : } {b : } {p : } (hb : b 0) (hp : ) (h : a.factors b.factors) :
p.count a.factors p.count b.factors
theorem Associates.count_le_count_of_le {α : Type u_1} [] [(p : ) → ] {a : } {b : } {p : } (hb : b 0) (hp : ) (h : a b) :
p.count a.factors p.count b.factors
theorem Associates.prod_le {α : Type u_1} [] {a : } {b : } :
a.prod b.prod a b
noncomputable instance Associates.instSup {α : Type u_1} :
Sup ()
Equations
• Associates.instSup = { sup := fun (a b : ) => (a.factors b.factors).prod }
noncomputable instance Associates.instInf {α : Type u_1} :
Inf ()
Equations
• Associates.instInf = { inf := fun (a b : ) => (a.factors b.factors).prod }
noncomputable instance Associates.instLattice {α : Type u_1} :
Equations
• Associates.instLattice = let __src := Associates.instPartialOrder; Lattice.mk
theorem Associates.sup_mul_inf {α : Type u_1} (a : ) (b : ) :
(a b) * (a b) = a * b
theorem Associates.dvd_of_mem_factors {α : Type u_1} {a : } {p : } (hm : p a.factors) :
p a
theorem Associates.dvd_of_mem_factors' {α : Type u_1} {a : α} {p : } {hp : } {hz : a 0} (h_mem : p, hp ) :
theorem Associates.mem_factors'_of_dvd {α : Type u_1} {a : α} {p : α} (ha0 : a 0) (hp : ) (hd : p a) :
,
theorem Associates.mem_factors'_iff_dvd {α : Type u_1} {a : α} {p : α} (ha0 : a 0) (hp : ) :
, p a
theorem Associates.mem_factors_of_dvd {α : Type u_1} {a : α} {p : α} (ha0 : a 0) (hp : ) (hd : p a) :
().factors
theorem Associates.mem_factors_iff_dvd {α : Type u_1} {a : α} {p : α} (ha0 : a 0) (hp : ) :
().factors p a
theorem Associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} {a : α} {b : α} (ha : a 0) (hb : b 0) (h : 1) :
∃ (p : α), p a p b
theorem Associates.coprime_iff_inf_one {α : Type u_1} {a : α} {b : α} (ha0 : a 0) (hb0 : b 0) :
= 1 ∀ {d : α}, d ad b¬
theorem Associates.factors_self {α : Type u_1} [] {p : } (hp : ) :
p.factors = {p, hp}
theorem Associates.factors_prime_pow {α : Type u_1} [] {p : } (hp : ) (k : ) :
(p ^ k).factors = (Multiset.replicate k p, hp)
theorem Associates.prime_pow_le_iff_le_bcount {α : Type u_1} [] {m : } {p : } (h₁ : m 0) (h₂ : ) {k : } :
p ^ k m k Associates.bcount p, h₂ m.factors
theorem Associates.prime_pow_dvd_iff_le {α : Type u_1} [] [(p : ) → ] {m : } {p : } (h₁ : m 0) (h₂ : ) {k : } :
p ^ k m k p.count m.factors
theorem Associates.le_of_count_ne_zero {α : Type u_1} [] [(p : ) → ] {m : } {p : } (h0 : m 0) (hp : ) :
p.count m.factors 0p m
theorem Associates.count_ne_zero_iff_dvd {α : Type u_1} [] [(p : ) → ] {a : α} {p : α} (ha0 : a 0) (hp : ) :
().count ().factors 0 p a
theorem Associates.count_self {α : Type u_1} [(p : ) → ] [] [] {p : } (hp : ) :
p.count p.factors = 1
theorem Associates.count_eq_zero_of_ne {α : Type u_1} [(p : ) → ] [] {p : } {q : } (hp : ) (hq : ) (h : p q) :
p.count q.factors = 0
theorem Associates.count_mul {α : Type u_1} [(p : ) → ] [] {a : } (ha : a 0) {b : } (hb : b 0) {p : } (hp : ) :
p.count (a * b).factors = p.count a.factors + p.count b.factors
theorem Associates.count_of_coprime {α : Type u_1} [(p : ) → ] [] {a : } (ha : a 0) {b : } (hb : b 0) (hab : ∀ (d : ), d ad b¬) {p : } (hp : ) :
p.count a.factors = 0 p.count b.factors = 0
theorem Associates.count_mul_of_coprime {α : Type u_1} [(p : ) → ] [] {a : } {b : } (hb : b 0) {p : } (hp : ) (hab : ∀ (d : ), d ad b¬) :
p.count a.factors = 0 p.count a.factors = p.count (a * b).factors
theorem Associates.count_mul_of_coprime' {α : Type u_1} [(p : ) → ] [] {a : } {b : } {p : } (hp : ) (hab : ∀ (d : ), d ad b¬) :
p.count (a * b).factors = p.count a.factors p.count (a * b).factors = p.count b.factors
theorem Associates.dvd_count_of_dvd_count_mul {α : Type u_1} [(p : ) → ] [] {a : } {b : } (hb : b 0) {p : } (hp : ) (hab : ∀ (d : ), d ad b¬) {k : } (habk : k p.count (a * b).factors) :
k p.count a.factors
@[simp]
theorem Associates.factors_one {α : Type u_1} [] :
@[simp]
theorem Associates.pow_factors {α : Type u_1} [] {a : } {k : } :
(a ^ k).factors = k a.factors
theorem Associates.count_pow {α : Type u_1} [(p : ) → ] [] [] {a : } (ha : a 0) {p : } (hp : ) (k : ) :
p.count (a ^ k).factors = k * p.count a.factors
theorem Associates.dvd_count_pow {α : Type u_1} [(p : ) → ] [] [] {a : } (ha : a 0) {p : } (hp : ) (k : ) :
k p.count (a ^ k).factors
theorem Associates.is_pow_of_dvd_count {α : Type u_1} [(p : ) → ] [] {a : } (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} [(p : ) → ] [] {p : } {a : } (hp : ) {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} [(p : ) → ] [] {a : } {p : } (hp : ) [(n : ) → Decidable (a p ^ n)] {n : } (h : a p ^ n) :
= p.count a.factors
theorem Associates.eq_pow_of_mul_eq_pow {α : Type u_1} {a : } {b : } {c : } (ha : a 0) (hb : b 0) (hab : ∀ (d : ), d ad 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 : } (hp : ) [(n : ) → Decidable (a p ^ n)] {n : } (h : a p ^ n) :
a = p ^

The only divisors of prime powers are prime powers.

noncomputable def UniqueFactorizationMonoid.toGCDMonoid (α : Type u_2) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• = let __src := inst;
Instances For
Equations
• =
noncomputable def UniqueFactorizationMonoid.fintypeSubtypeDvd {M : Type u_2} [] (y : M) (hy : y 0) :
Fintype { x : M // 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
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def factorization {α : Type u_1} [] (n : α) :

This returns the multiset of irreducible factors as a Finsupp.

Equations
• = Multiset.toFinsupp
Instances For
theorem factorization_eq_count {α : Type u_1} [] {n : α} {p : α} :
@[simp]
theorem factorization_zero {α : Type u_1} [] :
@[simp]
theorem factorization_one {α : Type u_1} [] :
@[simp]
theorem support_factorization {α : Type u_1} [] {n : α} :
().support = .toFinset

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

@[simp]
theorem factorization_mul {α : Type u_1} [] {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} [] {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} [] (a : α) (b : α) (ha : a 0) (hb : b 0) (h : ) :
theorem Ideal.IsPrime.exists_mem_prime_of_ne_bot {R : Type u_2} [] [] {I : } (hI₂ : I.IsPrime) (hI : I ) :
xI,

Every non-zero prime ideal in a unique factorization domain contains a prime element.

Equations
theorem Nat.factors_eq (n : ) :
= n.factors
theorem Nat.factors_multiset_prod_of_irreducible {s : } (h : xs, ) :
theorem induction_on_primes {P : } (h₀ : P 0) (h₁ : P 1) (h : ∀ (p a : ), p.PrimeP aP (p * a)) (n : ) :
P n