# Unique factorization and normalization #

## Main definitions #

- `UniqueFactorizationMonoid.normalizedFactors`: choose a multiset of prime factors that are unique by normalizing them.
- `UniqueFactorizationMonoid.normalizationMonoid`: choose a way of normalizing the elements of a UFM

source
noncomputable def UniqueFactorizationMonoid.normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) :
Multiset α

Noncomputably determines the multiset of prime factors.

Equations

- UniqueFactorizationMonoid.normalizedFactors a = Multiset.map (⇑normalize) (UniqueFactorizationMonoid.factors a)

Instances For

source
@[simp]
theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Subsingleton M ˣ] (x : M) :
factors x = normalizedFactors x

An arbitrary choice of factors of `x : M` is exactly the (unique) normalized set of factors, if `M` has a trivial group of units.

source
theorem UniqueFactorizationMonoid.prod_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) :
Associated (normalizedFactors a).prod a
source
theorem UniqueFactorizationMonoid.prod_normalizedFactors_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) :
(normalizedFactors a).prod = normalize a
source
theorem UniqueFactorizationMonoid.prime_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :
x ∈ normalizedFactors a → Prime x
source
theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :
x ∈ normalizedFactors a → Irreducible x
source
theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :
x ∈ normalizedFactors a → normalize x = x
source
theorem UniqueFactorizationMonoid.normalizedFactors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) :
normalizedFactors a = {normalize a}
source
theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a p : α) :
p ∈ normalizedFactors a → ∀ q ∈ normalizedFactors a, p ∣ q → p = q
source
theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
p ∣ a → ∃ q ∈ normalizedFactors a, Associated p q
source
theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :
∃ (p : α), p ∈ normalizedFactors x
source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] :
normalizedFactors 0 = 0
source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] :
normalizedFactors 1 = 0
source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) :
normalizedFactors (x ^ n) = n • normalizedFactors x
source
theorem Irreducible.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) :
UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
source
theorem UniqueFactorizationMonoid.normalizedFactors_prod_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) :
normalizedFactors s.prod = Multiset.map (⇑normalize) s
source
theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y
source
theorem Associated.normalizedFactors_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) :
UniqueFactorizationMonoid.normalizedFactors a = UniqueFactorizationMonoid.normalizedFactors b
source
theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
Associated x y ↔ normalizedFactors x = normalizedFactors y
source
theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) :
normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
source
theorem UniqueFactorizationMonoid.zero_notMem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) :
0 ∉ normalizedFactors x
source
theorem UniqueFactorizationMonoid.ne_zero_of_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x a : α} (hx : x ∈ normalizedFactors a) :
x ≠ 0
source
@[deprecated UniqueFactorizationMonoid.zero_notMem_normalizedFactors (since := "2025-05-23")]
theorem UniqueFactorizationMonoid.zero_not_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) :
0 ∉ normalizedFactors x

Alias of `UniqueFactorizationMonoid.zero_notMem_normalizedFactors`.

source
theorem UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (H : p ∈ normalizedFactors a) :
p ∣ a
source
@[deprecated UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors (since := "2025-08-26")]
theorem UniqueFactorizationMonoid.dvd_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (H : p ∈ normalizedFactors a) :
p ∣ a

Alias of `UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors`.

source
theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton α ˣ] {p x : α} (hx : x ≠ 0) :
p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x
source
theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff' {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p x : α} (h : x ≠ 0) :
p ∈ normalizedFactors x ↔ Irreducible p ∧ normalize p = p ∧ p ∣ x
source
theorem UniqueFactorizationMonoid.disjoint_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (hc : IsRelPrime a b) :
Disjoint (normalizedFactors a) (normalizedFactors b)

Relatively prime elements have disjoint prime factors (as multisets).

source
theorem UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p r : α} (h : ∀ {m : α}, m ∈ normalizedFactors r → m = p) (hr : r ≠ 0) :
∃ (i : ℕ), Associated (p ^ i) r
source
theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton α ˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) :
normalizedFactors m.prod = m
source
theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b c : α} (ha : a ∈ normalizedFactors c) (hb : b ∈ normalizedFactors c) (h : Associated a b) :
a = b
source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) :
0 < normalizedFactors x ↔ ¬IsUnit x
source
theorem UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) :
normalizedFactors x = 0 ↔ IsUnit x

The multiset of normalized factors of `x` is nil if and only if `x` is a unit. The converse is true without the nonzero assumption, see `normalizedFactors_of_isUnit`.

source
theorem UniqueFactorizationMonoid.normalizedFactors_of_isUnit {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : IsUnit x) :
normalizedFactors x = 0

If `x` is a unit, then the multiset of normalized factors of `x` is nil. The converse is true with a nonzero assumption, see `normalizedFactors_eq_zero_iff`.

source
theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y
source
theorem UniqueFactorizationMonoid.normalizedFactors_multiset_prod {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : 0 ∉ s) :
normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
source
def UniqueFactorizationMonoid.normalizedFactorsEquiv {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} (he : ∀ (x : α), normalize (f x) = f (normalize x)) (a : α) :
{ x : α // x ∈ normalizedFactors a } ≃ { y : β // y ∈ normalizedFactors (f a) }

If the monoid equiv `f : α ≃* β` commutes with `normalize` then, for `a : α`, it yields a bijection between the `normalizedFactors` of `a` and of `f a`.

Equations

- UniqueFactorizationMonoid.normalizedFactorsEquiv he a = (↑f).subtypeEquiv ⋯

Instances For

source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_apply {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a p : α} (hp : p ∈ normalizedFactors a) :
↑((normalizedFactorsEquiv he a) ⟨p, hp⟩) = f p
source
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a : α} {q : β} (hq : q ∈ normalizedFactors (f a)) :
↑((normalizedFactorsEquiv he a).symm ⟨q, hq⟩) = (↑f).symm q
source
noncomputable def UniqueFactorizationMonoid.normalizationMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :
NormalizationMonoid α

Noncomputably defines a `normalizationMonoid` structure on a `UniqueFactorizationMonoid`.

Equations

- One or more equations did not get rendered due to their size.

Instances For