# Unique factorization #

## Main Definitions #

- `WfDvdMonoid` holds for `Monoid`s for which a strict divisibility relation is well-founded.
- `UniqueFactorizationMonoid` holds for `WfDvdMonoid`s where `Irreducible` is equivalent to `Prime`

source
@[reducible, inline]
abbrev WfDvdMonoid (α : Type u_2) [CommMonoidWithZero α] :
Prop

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.

Equations

- WfDvdMonoid α = IsWellFounded α DvdNotUnit

Instances For

source
theorem wellFounded_dvdNotUnit {α : Type u_2} [CommMonoidWithZero α] [h : WfDvdMonoid α] :
WellFounded DvdNotUnit
source
theorem WfDvdMonoid.exists_irreducible_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a : α} (ha : ¬IsUnit a) (ha0 : a ≠ 0) :
∃ (i : α), Irreducible i ∧ i ∣ a
source
theorem WfDvdMonoid.induction_on_irreducible {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {motive : α → Prop} (a : α) (zero : motive 0) (unit : ∀ (u : α), IsUnit u → motive u) (mul : ∀ (a i : α), a ≠ 0 → Irreducible i → motive a → motive (i * a)) :
motive a
source
theorem WfDvdMonoid.exists_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) :
a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a
source
theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) (hn0 : a ≠ 0) :
¬IsUnit a ↔ ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅
source
theorem WfDvdMonoid.isRelPrime_of_no_irreducible_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ (z : α), Irreducible z → z ∣ x → ¬z ∣ y) :
IsRelPrime x y
source
class UniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends IsWellFounded α DvdNotUnit :
Prop

Unique factorization monoids are defined as `CancelCommMonoidWithZero`s 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_existsUnique_irreducible_factors`

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

- wf : WellFounded DvdNotUnit
- irreducible_iff_prime {a : α} : Irreducible a ↔ Prime a

Instances

source
@[instance 100]
instance ufm_of_decomposition_of_wfDvdMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [WfDvdMonoid α] [DecompositionMonoid α] :
UniqueFactorizationMonoid α
source
theorem UniqueFactorizationMonoid.exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :
a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a
source
theorem UniqueFactorizationMonoid.exists_prime_iff {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :
(∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x
source
theorem UniqueFactorizationMonoid.induction_on_prime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), IsUnit x → P x) (h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)) :
P a
source
instance UniqueFactorizationMonoid.instDecompositionMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :
DecompositionMonoid α
source
noncomputable def UniqueFactorizationMonoid.factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :
Multiset α

Noncomputably determines the multiset of prime factors.

Equations

- UniqueFactorizationMonoid.factors a = if h : a = 0 then 0 else Classical.choose ⋯

Instances For

source
theorem UniqueFactorizationMonoid.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) :
Associated (factors a).prod a
source
@[simp]
theorem UniqueFactorizationMonoid.factors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :
factors 0 = 0
source
theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p a : α} (h : p ∈ factors a) :
a ≠ 0
source
theorem UniqueFactorizationMonoid.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p a : α} (h : p ∈ factors a) :
p ∣ a
source
theorem UniqueFactorizationMonoid.prime_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (x : α) (hx : x ∈ factors a) :
Prime x
source
theorem UniqueFactorizationMonoid.irreducible_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (x : α) :
x ∈ factors a → Irreducible x