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

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)

@[simp]

theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Subsingleton Mˣ] (x : M) : UniqueFactorizationMonoid.factors x = UniqueFactorizationMonoid.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.

theorem UniqueFactorizationMonoid.normalizedFactors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a

theorem UniqueFactorizationMonoid.prime_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.normalizedFactors a → Prime x

theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.normalizedFactors a → Irreducible x

theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ UniqueFactorizationMonoid.normalizedFactors a → normalize x = x

theorem UniqueFactorizationMonoid.normalizedFactors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) : UniqueFactorizationMonoid.normalizedFactors a = {normalize a}

theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a p : α) : p ∈ UniqueFactorizationMonoid.normalizedFactors a → ∀ q ∈ UniqueFactorizationMonoid.normalizedFactors a, p ∣ q → p = q

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.normalizedFactors a, Associated p q

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ (p : α), p ∈ UniqueFactorizationMonoid.normalizedFactors x

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid.normalizedFactors 0 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid.normalizedFactors 1 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : UniqueFactorizationMonoid.normalizedFactors (x * y) = UniqueFactorizationMonoid.normalizedFactors x + UniqueFactorizationMonoid.normalizedFactors y

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) : UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x

theorem Irreducible.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) : UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

theorem UniqueFactorizationMonoid.normalizedFactors_prod_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) : UniqueFactorizationMonoid.normalizedFactors s.prod = Multiset.map (⇑normalize) s

theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y

theorem Associated.normalizedFactors_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : UniqueFactorizationMonoid.normalizedFactors a = UniqueFactorizationMonoid.normalizedFactors b

theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : Associated x y ↔ UniqueFactorizationMonoid.normalizedFactors x = UniqueFactorizationMonoid.normalizedFactors y

theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) : UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

theorem UniqueFactorizationMonoid.zero_not_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) : 0 ∉ UniqueFactorizationMonoid.normalizedFactors x

theorem UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (H : p ∈ UniqueFactorizationMonoid.normalizedFactors a) : p ∣ a

theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton αˣ] {p x : α} (hx : x ≠ 0) : p ∈ UniqueFactorizationMonoid.normalizedFactors x ↔ Prime p ∧ p ∣ x

theorem UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p r : α} (h : ∀ {m : α}, m ∈ UniqueFactorizationMonoid.normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ (i : ℕ), Associated (p ^ i) r

theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton αˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) : UniqueFactorizationMonoid.normalizedFactors m.prod = m

theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b c : α} (ha : a ∈ UniqueFactorizationMonoid.normalizedFactors c) (hb : b ∈ UniqueFactorizationMonoid.normalizedFactors c) (h : Associated a b) : a = b

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) : 0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x

theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : DvdNotUnit x y ↔ UniqueFactorizationMonoid.normalizedFactors x < UniqueFactorizationMonoid.normalizedFactors y

theorem UniqueFactorizationMonoid.normalizedFactors_multiset_prod {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : 0 ∉ s) : UniqueFactorizationMonoid.normalizedFactors s.prod = (Multiset.map UniqueFactorizationMonoid.normalizedFactors s).sum

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.