@[class]
- factors : α → multiset α
- factors_prod : ∀ {a : α}, a ≠ 0 → associated (unique_factorization_domain.factors a).prod a
- prime_factors : ∀ {a : α}, a ≠ 0 → ∀ (x : α), x ∈ unique_factorization_domain.factors a → prime x
Unique factorization domains.
In a unique factorization domain each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements.
This is equivalent to defining a unique factorization domain as a domain in which each element (except zero) is non-uniquely represented as a multiset of prime factors. This definition is used.
To define a UFD using the traditional definition in terms of multisets
of irreducible factors, use the definition of_unique_irreducible_factorization
theorem
unique_factorization_domain.induction_on_prime
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{P : α → Prop}
(a : α) :
theorem
unique_factorization_domain.factors_irreducible
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a : α} :
irreducible a → (∃ (p : α), associated a p ∧ unique_factorization_domain.factors a = p :: 0)
theorem
unique_factorization_domain.irreducible_iff_prime
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{p : α} :
irreducible p ↔ prime p
theorem
unique_factorization_domain.irreducible_factors
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a : α}
(a_1 : a ≠ 0)
(x : α) :
theorem
unique_factorization_domain.unique
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{f g : multiset α} :
(∀ (x : α), x ∈ f → irreducible x) → (∀ (x : α), x ∈ g → irreducible x) → associated f.prod g.prod → multiset.rel associated f g
- factors : α → multiset α
- factors_prod : ∀ {a : α}, a ≠ 0 → associated (c.factors a).prod a
- irreducible_factors : ∀ {a : α}, a ≠ 0 → ∀ (x : α), x ∈ c.factors a → irreducible x
- unique : ∀ {f g : multiset α}, (∀ (x : α), x ∈ f → irreducible x) → (∀ (x : α), x ∈ g → irreducible x) → associated f.prod g.prod → multiset.rel associated f g
theorem
unique_factorization_domain.exists_mem_factors_of_dvd
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a p : α} :
a ≠ 0 → irreducible p → p ∣ a → (∃ (q : α) (H : q ∈ unique_factorization_domain.factors a), associated p q)
def
unique_factorization_domain.of_unique_irreducible_factorization
{α : Type u_1}
[integral_domain α] :
Equations
factor_set α representation elements of unique factorization domain as multisets.
multiset α produced by factors are only unique up to associated elements, while the multisets in
factor_set α are unqiue by equality and restricted to irreducible elements. This gives us a
representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete
lattice struture. Infimum is the greatest common divisor and supremum is the least common multiple.
Equations
- associates.factor_set α = with_top (multiset {a // irreducible a})
theorem
associates.factor_set.coe_add
{α : Type u_1}
[integral_domain α]
{a b : multiset {a // irreducible a}} :
theorem
associates.factor_set.sup_add_inf_eq_add
{α : Type u_1}
[integral_domain α]
[decidable_eq (associates α)]
(a b : associates.factor_set α) :
Equations
@[simp]
theorem
associates.prod_coe
{α : Type u_1}
[integral_domain α]
{s : multiset {a // irreducible a}} :
@[simp]
theorem
associates.unique'
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{p q : multiset (associates α)} :
(∀ (a : associates α), a ∈ p → irreducible a) → (∀ (a : associates α), a ∈ q → irreducible a) → p.prod = q.prod → p = q
theorem
associates.prod_le_prod_iff_le
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{p q : multiset (associates α)} :
(∀ (a : associates α), a ∈ p → irreducible a) → (∀ (a : associates α), a ∈ q → irreducible a) → (p.prod ≤ q.prod ↔ p ≤ q)
def
associates.factors'
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
(a : α) :
a ≠ 0 → multiset {a // irreducible a}
Equations
- associates.factors' a ha = multiset.pmap (λ (a : α) (ha : irreducible a), ⟨associates.mk a, _⟩) (unique_factorization_domain.factors a) _
@[simp]
theorem
associates.map_subtype_coe_factors'
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a : α}
(ha : a ≠ 0) :
theorem
associates.factors'_cong
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a b : α}
(ha : a ≠ 0)
(hb : b ≠ 0) :
associated a b → associates.factors' a ha = associates.factors' b hb
def
associates.factors
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)] :
Equations
- a.factors = dite (a = 0) (λ (h : a = 0), ⊤) (λ (h : ¬a = 0), quotient.hrec_on a (λ (x : α) (h : ¬⟦x⟧ = 0), option.some (associates.factors' x _)) associates.factors._proof_2 h)
@[simp]
theorem
associates.factors_0
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)] :
@[simp]
theorem
associates.factors_mk
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
(a : α)
(h : a ≠ 0) :
(associates.mk a).factors = ↑(associates.factors' a h)
theorem
associates.prod_factors
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
(s : associates.factor_set α) :
theorem
associates.factors_prod
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
(a : associates α) :
theorem
associates.eq_of_factors_eq_factors
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
{a b : associates α} :
theorem
associates.eq_of_prod_eq_prod
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a b : associates.factor_set α} :
@[simp]
theorem
associates.factors_mul
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
(a b : associates α) :
theorem
associates.factors_mono
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
{a b : associates α} :
theorem
associates.factors_le
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
{a b : associates α} :
theorem
associates.prod_le
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
{a b : associates.factor_set α} :
@[instance]
def
associates.has_sup
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)] :
has_sup (associates α)
Equations
- associates.has_sup = {sup := λ (a b : associates α), (a.factors ⊔ b.factors).prod}
@[instance]
def
associates.has_inf
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)] :
has_inf (associates α)
Equations
- associates.has_inf = {inf := λ (a b : associates α), (a.factors ⊓ b.factors).prod}
@[instance]
def
associates.bounded_lattice
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)] :
Equations
- associates.bounded_lattice = {sup := has_sup.sup associates.has_sup, le := partial_order.le associates.partial_order, lt := partial_order.lt associates.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf associates.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top associates.order_top, le_top := _, bot := order_bot.bot associates.order_bot, bot_le := _}
theorem
associates.sup_mul_inf
{α : Type u_1}
[integral_domain α]
[unique_factorization_domain α]
[dec : decidable_eq (associates α)]
(a b : associates α) :
def
unique_factorization_domain.to_gcd_monoid
(α : Type u_1)
[integral_domain α]
[unique_factorization_domain α]
[normalization_monoid α]
[decidable_eq (associates α)] :
to_gcd_monoid constructs a GCD monoid out of a normalization on a
unique factorization domain.
Equations
- unique_factorization_domain.to_gcd_monoid α = {norm_unit := normalization_monoid.norm_unit _inst_3, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _, gcd := λ (a b : α), (associates.mk a ⊓ associates.mk b).out, lcm := λ (a b : α), (associates.mk a ⊔ associates.mk b).out, gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, normalize_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}
theorem
unique_factorization_domain.no_factors_of_no_prime_factors
{R : Type u_2}
[integral_domain R]
[unique_factorization_domain R]
{a b : R}
(ha : a ≠ 0)
(h : ∀ {d : R}, d ∣ a → d ∣ b → ¬prime d)
{d : R} :
theorem
unique_factorization_domain.dvd_of_dvd_mul_left_of_no_prime_factors
{R : Type u_2}
[integral_domain R]
[unique_factorization_domain R]
{a b c : R} :
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_domain.dvd_of_dvd_mul_right_of_no_prime_factors
{R : Type u_2}
[integral_domain R]
[unique_factorization_domain R]
{a b c : R} :
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_domain.exists_reduced_factors
{R : Type u_2}
[integral_domain R]
[unique_factorization_domain 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_domain.exists_reduced_factors'
{R : Type u_2}
[integral_domain R]
[unique_factorization_domain R]
(a b : R) :