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) [CommMonoidWithZero α] :

wellFounded_dvdNotUnit : WellFounded DvdNotUnit

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

source

instance IsNoetherianRing.wfDvdMonoid {α : Type u_1} [CommRing α] [IsDomain α] [IsNoetherianRing α] :

WfDvdMonoid α

Equations

@IsNoetherianRing.wfDvdMonoid = @IsNoetherianRing.wfDvdMonoid.proof_1

source

theorem WfDvdMonoid.of_wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] :

WfDvdMonoid (Associates α) → WfDvdMonoid α

source

instance WfDvdMonoid.wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] :

WfDvdMonoid (Associates α)

Equations

@WfDvdMonoid.wfDvdMonoid_associates = @WfDvdMonoid.wfDvdMonoid_associates.proof_1

source

theorem WfDvdMonoid.wellFounded_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] :

WellFounded fun x x_1 => x < x_1

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 α] {P : α → Prop} (a : α) (h0 : P 0) (hu : ∀ (u : α), IsUnit u → P u) (hi : ∀ (a i : α), a ≠ 0 → Irreducible i → P a → P (i * a)) :

P a

source

theorem WfDvdMonoid.exists_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) :

a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a

source

theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) (hn0 : a ≠ 0) :

¬IsUnit a ↔ ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f = a ∧ f ≠ ∅

source

theorem WfDvdMonoid.of_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] (h : WellFounded fun x x_1 => x < x_1) :

WfDvdMonoid α

source

theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} [CancelCommMonoidWithZero α] :

WfDvdMonoid α ↔ WellFounded fun x x_1 => x < x_1

source

class UniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] extends WfDvdMonoid :

Prop

wellFounded_dvdNotUnit : WellFounded DvdNotUnit
irreducible_iff_prime : ∀ {a : α}, Irreducible a ↔ Prime a

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

Instances

source

@[reducible]

theorem ufm_of_gcd_of_wfDvdMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [WfDvdMonoid α] [GCDMonoid α] :

UniqueFactorizationMonoid α

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

source

instance Associates.ufm {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid (Associates α)

Equations

@Associates.ufm = @Associates.ufm.proof_1

source

theorem UniqueFactorizationMonoid.exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) :

a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a

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

theorem prime_factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] {f : Multiset α} {g : Multiset α} :

(∀ (x : α), x ∈ f → Prime x) → (∀ (x : α), x ∈ g → Prime x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g

source

theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {f : Multiset α} {g : Multiset α} (hf : ∀ (x : α), x ∈ f → Irreducible x) (hg : ∀ (x : α), x ∈ g → Irreducible x) (h : Associated (Multiset.prod f) (Multiset.prod g)) :

Multiset.Rel Associated f g

source

theorem prime_factors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] {a : α} {f : Multiset α} (ha : Irreducible a) (pfa : (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a) :

∃ p, Associated a p ∧ f = {p}

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

source

theorem WfDvdMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a) :

WfDvdMonoid α

source

theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a) {p : α} :

Irreducible p ↔ Prime p

source

theorem UniqueFactorizationMonoid.of_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a) :

UniqueFactorizationMonoid α

source

theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} [CancelCommMonoidWithZero α] :

UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a

source

theorem MulEquiv.uniqueFactorizationMonoid {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [CancelCommMonoidWithZero β] (e : α ≃* β) (hα : UniqueFactorizationMonoid α) :

UniqueFactorizationMonoid β

source

theorem MulEquiv.uniqueFactorizationMonoid_iff {α : Type u_1} {β : Type u_2} [CancelCommMonoidWithZero α] [CancelCommMonoidWithZero β] (e : α ≃* β) :

UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β

source

theorem irreducible_iff_prime_of_exists_unique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a) (uif : ∀ (f g : Multiset α), (∀ (x : α), x ∈ f → Irreducible x) → (∀ (x : α), x ∈ g → Irreducible x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g) (p : α) :

Irreducible p ↔ Prime p

source

theorem UniqueFactorizationMonoid.of_exists_unique_irreducible_factors {α : Type u_1} [CancelCommMonoidWithZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a) (uif : ∀ (f g : Multiset α), (∀ (x : α), x ∈ f → Irreducible x) → (∀ (x : α), x ∈ g → Irreducible x) → Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g) :

UniqueFactorizationMonoid α

source

noncomputable def UniqueFactorizationMonoid.factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] (a : α) :

Multiset α

Noncomputably determines the multiset of prime factors.

Equations

UniqueFactorizationMonoid.factors a = if h : a = 0 then 0 else Classical.choose (_ : ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Associated (Multiset.prod f) a)

Instances For

source

theorem UniqueFactorizationMonoid.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) :

Associated (Multiset.prod (UniqueFactorizationMonoid.factors a)) a

source

theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {p : α} {a : α} (h : p ∈ UniqueFactorizationMonoid.factors a) :

a ≠ 0

source

theorem UniqueFactorizationMonoid.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {p : α} {a : α} (h : p ∈ UniqueFactorizationMonoid.factors a) :

p ∣ a

source

theorem UniqueFactorizationMonoid.prime_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} (x : α) (hx : x ∈ UniqueFactorizationMonoid.factors a) :

Prime x

source

theorem UniqueFactorizationMonoid.irreducible_of_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.factors a → Irreducible x

source

@[simp]

theorem UniqueFactorizationMonoid.factors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.factors 0 = 0

source

@[simp]

theorem UniqueFactorizationMonoid.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.factors 1 = 0

source

theorem UniqueFactorizationMonoid.exists_mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

p ∣ a → ∃ q, q ∈ UniqueFactorizationMonoid.factors a ∧ Associated p q

source

theorem UniqueFactorizationMonoid.exists_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :

∃ p, p ∈ UniqueFactorizationMonoid.factors x

source

theorem UniqueFactorizationMonoid.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {x : α} {y : α} (hx : x ≠ 0) (hy : y ≠ 0) :

Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x * y)) (UniqueFactorizationMonoid.factors x + UniqueFactorizationMonoid.factors y)

source

theorem UniqueFactorizationMonoid.factors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) :

Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x ^ n)) (n • UniqueFactorizationMonoid.factors x)

source

@[simp]

theorem UniqueFactorizationMonoid.factors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) :

0 < UniqueFactorizationMonoid.factors x ↔ ¬IsUnit x

source

noncomputable def UniqueFactorizationMonoid.normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [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] [DecidableEq M] [UniqueFactorizationMonoid M] [Unique 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.

source

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

Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a

source

theorem UniqueFactorizationMonoid.prime_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.normalizedFactors a → Prime x

source

theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.normalizedFactors a → Irreducible x

source

theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) :

x ∈ UniqueFactorizationMonoid.normalizedFactors a → ↑normalize x = x

source

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

UniqueFactorizationMonoid.normalizedFactors a = {↑normalize a}

source

theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) (p : α) :

p ∈ UniqueFactorizationMonoid.normalizedFactors a → ∀ (q : α), q ∈ UniqueFactorizationMonoid.normalizedFactors a → p ∣ q → p = q

source

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

p ∣ a → ∃ q, q ∈ UniqueFactorizationMonoid.normalizedFactors a ∧ Associated p q

source

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :

∃ p, p ∈ UniqueFactorizationMonoid.normalizedFactors x

source

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.normalizedFactors 0 = 0

source

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_one {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] :

UniqueFactorizationMonoid.normalizedFactors 1 = 0

source

@[simp]

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

UniqueFactorizationMonoid.normalizedFactors (x * y) = UniqueFactorizationMonoid.normalizedFactors x + UniqueFactorizationMonoid.normalizedFactors y

source

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) :

UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x

source

theorem Irreducible.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [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 α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : ∀ (a : α), a ∈ s → Irreducible a) :

UniqueFactorizationMonoid.normalizedFactors (Multiset.prod s) = Multiset.map (↑normalize) s

source

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

x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y

source

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

Associated x y ↔ UniqueFactorizationMonoid.normalizedFactors x = UniqueFactorizationMonoid.normalizedFactors y

source

theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) :

UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (↑normalize p)

source

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

¬0 ∈ UniqueFactorizationMonoid.normalizedFactors x

source

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

p ∣ a

source

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

∃ i, Associated (p ^ i) r

source

theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Nontrivial α] [Unique αˣ] {m : Multiset α} (h : ∀ (p : α), p ∈ m → Prime p) :

UniqueFactorizationMonoid.normalizedFactors (Multiset.prod m) = m

source

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

a = b

source

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) :

0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x

source

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

DvdNotUnit x y ↔ UniqueFactorizationMonoid.normalizedFactors x < UniqueFactorizationMonoid.normalizedFactors y

source

noncomputable def UniqueFactorizationMonoid.normalizationMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] [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

source

noncomputable instance UniqueFactorizationMonoid.instInhabitedNormalizationMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] [UniqueFactorizationMonoid α] :

Inhabited (NormalizationMonoid α)

Equations

UniqueFactorizationMonoid.instInhabitedNormalizationMonoid = { default := UniqueFactorizationMonoid.normalizationMonoid }

source

theorem UniqueFactorizationMonoid.no_factors_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} (ha : a ≠ 0) (h : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) {d : R} :

d ∣ a → d ∣ b → IsUnit d

source

theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} {c : R} (ha : a ≠ 0) :

(∀ {d : R}, d ∣ a → d ∣ c → ¬Prime d) → a ∣ b * c → a ∣ 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.

source

theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} {b : R} {c : R} (ha : a ≠ 0) (no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) :

a ∣ b * c → a ∣ 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.

source

theorem UniqueFactorizationMonoid.exists_reduced_factors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R) :

a ≠ 0 → ∀ (b : R), ∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ 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.

source

theorem UniqueFactorizationMonoid.exists_reduced_factors' {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R) (b : R) (hb : b ≠ 0) :

∃ a' b' c', (∀ {d : R}, d ∣ a' → d ∣ b' → IsUnit d) ∧ c' * a' = a ∧ c' * b' = b

source

theorem UniqueFactorizationMonoid.pow_right_injective {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} (ha0 : a ≠ 0) (ha1 : ¬IsUnit a) :

Function.Injective ((fun x x_1 => x ^ x_1) a)

source

theorem UniqueFactorizationMonoid.pow_eq_pow_iff {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {a : R} (ha0 : a ≠ 0) (ha1 : ¬IsUnit a) {i : ℕ} {j : ℕ} :

a ^ i = a ^ j ↔ i = j

source

theorem UniqueFactorizationMonoid.le_multiplicity_iff_replicate_le_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [dec_dvd : DecidableRel Dvd.dvd] [DecidableEq R] {a : R} {b : R} {n : ℕ} (ha : Irreducible a) (hb : b ≠ 0) :

↑n ≤ multiplicity a b ↔ Multiset.replicate n (↑normalize a) ≤ UniqueFactorizationMonoid.normalizedFactors b

source

theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [dec_dvd : DecidableRel Dvd.dvd] [DecidableEq R] {a : R} {b : R} (ha : Irreducible a) (hb : b ≠ 0) :

multiplicity a b = ↑(Multiset.count (↑normalize a) (UniqueFactorizationMonoid.normalizedFactors b))

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 _) _..

source

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [DecidableEq R] {p : R} {x : R} (hp : Irreducible p) (hnorm : ↑normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) :

Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

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.

source

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq' {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [DecidableEq R] {p : R} {x : R} (hp : p = 0 ∨ Irreducible p) (hnorm : ↑normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) :

Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n

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.

source

theorem UniqueFactorizationMonoid.max_power_factor {R : Type u_2} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] [Nontrivial R] [NormalizationMonoid R] [dec_dvd : DecidableRel Dvd.dvd] {a₀ : R} {x : R} (h : a₀ ≠ 0) (hx : Irreducible x) :

∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a

source

theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {s : Finset α} (i : α → ℕ) (p : α) (hps : ¬p ∈ s) (is_prime : ∀ (q : α), q ∈ insert p s → Prime q) (is_coprime : ∀ (q : α), q ∈ insert p s → ∀ (q' : α), q' ∈ insert p s → q ∣ q' → q = q') (q : α) :

q ∣ p ^ i p → (q ∣ Finset.prod s fun p' => p' ^ i p') → IsUnit q

source

theorem UniqueFactorizationMonoid.induction_on_prime_power {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (s : Finset α) (i : α → ℕ) (is_prime : ∀ (p : α), p ∈ s → Prime p) (is_coprime : ∀ (p : α), p ∈ s → ∀ (q : α), q ∈ s → p ∣ q → p = q) (h1 : ∀ {x : α}, IsUnit x → P x) (hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (x * y)) :

P (Finset.prod s 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.

source

theorem UniqueFactorizationMonoid.induction_on_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α) (h0 : P 0) (h1 : ∀ {x : α}, IsUnit x → P x) (hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → P x → P y → P (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 : α.

source

theorem UniqueFactorizationMonoid.multiplicative_prime_power {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CancelCommMonoidWithZero β] {f : α → β} (s : Finset α) (i : α → ℕ) (j : α → ℕ) (is_prime : ∀ (p : α), p ∈ s → Prime p) (is_coprime : ∀ (p : α), p ∈ s → ∀ (q : α), q ∈ s → p ∣ q → p = q) (h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → f (x * y) = f x * f y) :

f (Finset.prod s fun p => p ^ (i p + j p)) = f (Finset.prod s fun p => p ^ i p) * f (Finset.prod s 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.

source

theorem UniqueFactorizationMonoid.multiplicative_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CancelCommMonoidWithZero β] (f : α → β) (a : α) (b : α) (h0 : f 0 = 0) (h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, (∀ (p : α), p ∣ x → p ∣ y → IsUnit p) → 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.

source

@[reducible]

def Associates.FactorSet (α : Type u) [CancelCommMonoidWithZero α] :

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

Associates.FactorSet α = WithTop (Multiset { a // Irreducible a })

Instances For

source

theorem Associates.FactorSet.coe_add {α : Type u_1} [CancelCommMonoidWithZero α] {a : Multiset { a // Irreducible a }} {b : Multiset { a // Irreducible a }} :

↑(a + b) = ↑a + ↑b

source

theorem Associates.FactorSet.sup_add_inf_eq_add {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] (a : Associates.FactorSet α) (b : Associates.FactorSet α) :

a ⊔ b + a ⊓ b = a + b

source

def Associates.FactorSet.prod {α : Type u_1} [CancelCommMonoidWithZero α] :

Associates.FactorSet α → Associates α

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

Equations

Associates.FactorSet.prod x = match x with | none => 0 | some s => Multiset.prod (Multiset.map Subtype.val s)

Instances For

source

@[simp]

theorem Associates.prod_top {α : Type u_1} [CancelCommMonoidWithZero α] :

Associates.FactorSet.prod ⊤ = 0

source

@[simp]

theorem Associates.prod_coe {α : Type u_1} [CancelCommMonoidWithZero α] {s : Multiset { a // Irreducible a }} :

Associates.FactorSet.prod ↑s = Multiset.prod (Multiset.map Subtype.val s)

source

@[simp]

theorem Associates.prod_add {α : Type u_1} [CancelCommMonoidWithZero α] (a : Associates.FactorSet α) (b : Associates.FactorSet α) :

Associates.FactorSet.prod (a + b) = Associates.FactorSet.prod a * Associates.FactorSet.prod b

source

theorem Associates.prod_mono {α : Type u_1} [CancelCommMonoidWithZero α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} :

a ≤ b → Associates.FactorSet.prod a ≤ Associates.FactorSet.prod b

source

theorem Associates.FactorSet.prod_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (p : Associates.FactorSet α) :

Associates.FactorSet.prod p = 0 ↔ p = ⊤

source

def Associates.bcount {α : Type u_1} [CancelCommMonoidWithZero α] [DecidableEq (Associates α)] (p : { a // Irreducible a }) :

Associates.FactorSet α → ℕ

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

Equations

Associates.bcount p x = match x with | none => 0 | some s => Multiset.count p s

Instances For

source

def Associates.count {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] (p : Associates α) :

Associates.FactorSet α → ℕ

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

Associates.count p = if hp : Irreducible p then Associates.bcount { val := p, property := hp } else 0

Instances For

source

@[simp]

theorem Associates.count_some {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} (hp : Irreducible p) (s : Multiset { a // Irreducible a }) :

Associates.count p (some s) = Multiset.count { val := p, property := hp } s

source

@[simp]

theorem Associates.count_zero {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} (hp : Irreducible p) :

Associates.count p 0 = 0

source

theorem Associates.count_reducible {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [DecidableEq (Associates α)] {p : Associates α} (hp : ¬Irreducible p) :

Associates.count p = 0

source

def Associates.BfactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] :

{ a // Irreducible a } → Associates.FactorSet α → Prop

membership in a FactorSet (bundled version)

Equations

Associates.BfactorSetMem x✝ x = match x✝, x with | x, none => True | p, some l => p ∈ l

Instances For

source

def Associates.FactorSetMem {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] (p : Associates α) (s : Associates.FactorSet α) :

Prop

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

Associates.FactorSetMem p s = if hp : Irreducible p then Associates.BfactorSetMem { val := p, property := hp } s else False

Instances For

source

instance Associates.instMembershipAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZeroFactorSet {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] :

Membership (Associates α) (Associates.FactorSet α)

Equations

Associates.instMembershipAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZeroFactorSet = { mem := Associates.FactorSetMem }

source

@[simp]

theorem Associates.factorSetMem_eq_mem {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] (p : Associates α) (s : Associates.FactorSet α) :

Associates.FactorSetMem p s = (p ∈ s)

source

theorem Associates.mem_factorSet_top {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} {hp : Irreducible p} :

p ∈ ⊤

source

theorem Associates.mem_factorSet_some {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} {hp : Irreducible p} {l : Multiset { a // Irreducible a }} :

p ∈ ↑l ↔ { val := p, property := hp } ∈ l

source

theorem Associates.reducible_not_mem_factorSet {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : ¬Irreducible p) (s : Associates.FactorSet α) :

¬p ∈ s

source

theorem Associates.unique' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} :

(∀ (a : Associates α), a ∈ p → Irreducible a) → (∀ (a : Associates α), a ∈ q → Irreducible a) → Multiset.prod p = Multiset.prod q → p = q

source

theorem Associates.FactorSet.unique {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Associates.FactorSet α} {q : Associates.FactorSet α} (h : Associates.FactorSet.prod p = Associates.FactorSet.prod q) :

p = q

source

theorem Associates.prod_le_prod_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} (hp : ∀ (a : Associates α), a ∈ p → Irreducible a) (hq : ∀ (a : Associates α), a ∈ q → Irreducible a) :

Multiset.prod p ≤ Multiset.prod q ↔ p ≤ q

source

noncomputable def Associates.factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] (a : α) :

Multiset { a // Irreducible a }

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

Equations

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

Instances For

source

@[simp]

theorem Associates.map_subtype_coe_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} :

Multiset.map Subtype.val (Associates.factors' a) = Multiset.map Associates.mk (UniqueFactorizationMonoid.factors a)

source

theorem Associates.factors'_cong {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {b : α} (h : Associated a b) :

Associates.factors' a = Associates.factors' b

source

noncomputable def Associates.factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) :

Associates.FactorSet α

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

source

@[simp]

theorem Associates.factors_0 {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] :

Associates.factors 0 = ⊤

source

@[simp]

theorem Associates.factors_mk {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : α) (h : a ≠ 0) :

Associates.factors (Associates.mk a) = ↑(Associates.factors' a)

source

@[simp]

theorem Associates.factors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) :

Associates.FactorSet.prod (Associates.factors a) = a

source

theorem Associates.prod_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] (s : Associates.FactorSet α) :

Associates.factors (Associates.FactorSet.prod s) = s

source

theorem Associates.factors_subsingleton {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Subsingleton α] {a : Associates α} :

Associates.factors a = none

source

theorem Associates.factors_eq_none_iff_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} :

Associates.factors a = none ↔ a = 0

source

theorem Associates.factors_eq_some_iff_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} :

(∃ s, Associates.factors a = some s) ↔ a ≠ 0

source

theorem Associates.eq_of_factors_eq_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (h : Associates.factors a = Associates.factors b) :

a = b

source

theorem Associates.eq_of_prod_eq_prod {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} (h : Associates.FactorSet.prod a = Associates.FactorSet.prod b) :

a = b

source

theorem Associates.eq_factors_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : Associates α), Irreducible p → Associates.count p (Associates.factors a) = Associates.count p (Associates.factors b)) :

Associates.factors a = Associates.factors b

source

theorem Associates.eq_of_eq_counts {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (h : ∀ (p : Associates α), Irreducible p → Associates.count p (Associates.factors a) = Associates.count p (Associates.factors b)) :

a = b

source

theorem Associates.count_le_count_of_factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hb : b ≠ 0) (hp : Irreducible p) (h : Associates.factors a ≤ Associates.factors b) :

Associates.count p (Associates.factors a) ≤ Associates.count p (Associates.factors b)

source

@[simp]

theorem Associates.factors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) (b : Associates α) :

Associates.factors (a * b) = Associates.factors a + Associates.factors b

source

theorem Associates.factors_mono {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} :

a ≤ b → Associates.factors a ≤ Associates.factors b

source

theorem Associates.factors_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} :

Associates.factors a ≤ Associates.factors b ↔ a ≤ b

source

theorem Associates.count_le_count_of_le {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hb : b ≠ 0) (hp : Irreducible p) (h : a ≤ b) :

Associates.count p (Associates.factors a) ≤ Associates.count p (Associates.factors b)

source

theorem Associates.prod_le {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates.FactorSet α} {b : Associates.FactorSet α} :

Associates.FactorSet.prod a ≤ Associates.FactorSet.prod b ↔ a ≤ b

source

noncomputable instance Associates.instSupAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] :

Sup (Associates α)

Equations

Associates.instSupAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero = { sup := fun a b => Associates.FactorSet.prod (Associates.factors a ⊔ Associates.factors b) }

source

noncomputable instance Associates.instInfAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] :

Inf (Associates α)

Equations

Associates.instInfAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero = { inf := fun a b => Associates.FactorSet.prod (Associates.factors a ⊓ Associates.factors b) }

source

noncomputable instance Associates.instLatticeAssociatesToMonoidToMonoidWithZeroToCommMonoidWithZero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] :

Lattice (Associates α)

Equations

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

source

theorem Associates.sup_mul_inf {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] (a : Associates α) (b : Associates α) :

(a ⊔ b) * (a ⊓ b) = a * b

source

theorem Associates.dvd_of_mem_factors {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {p : Associates α} {hp : Irreducible p} (hm : p ∈ Associates.factors a) :

p ∣ a

source

theorem Associates.dvd_of_mem_factors' {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {p : Associates α} {hp : Irreducible p} {hz : a ≠ 0} (h_mem : { val := p, property := hp } ∈ Associates.factors' a) :

p ∣ Associates.mk a

source

theorem Associates.mem_factors'_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :

{ val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ Associates.factors' a

source

theorem Associates.mem_factors'_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

{ val := Associates.mk p, property := (_ : Irreducible (Associates.mk p)) } ∈ Associates.factors' a ↔ p ∣ a

source

theorem Associates.mem_factors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :

Associates.mk p ∈ Associates.factors (Associates.mk a)

source

theorem Associates.mem_factors_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

Associates.mk p ∈ Associates.factors (Associates.mk a) ↔ p ∣ a

source

theorem Associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : Associates.mk a ⊓ Associates.mk b ≠ 1) :

∃ p, Prime p ∧ p ∣ a ∧ p ∣ b

source

theorem Associates.coprime_iff_inf_one {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {b : α} (ha0 : a ≠ 0) (hb0 : b ≠ 0) :

Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

source

theorem Associates.factors_self {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) :

Associates.factors p = some {{ val := p, property := hp }}

source

theorem Associates.factors_prime_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) (k : ℕ) :

Associates.factors (p ^ k) = some (Multiset.replicate k { val := p, property := hp })

source

theorem Associates.prime_pow_dvd_iff_le {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {m : Associates α} {p : Associates α} (h₁ : m ≠ 0) (h₂ : Irreducible p) {k : ℕ} :

p ^ k ≤ m ↔ k ≤ Associates.count p (Associates.factors m)

source

theorem Associates.le_of_count_ne_zero {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {m : Associates α} {p : Associates α} (h0 : m ≠ 0) (hp : Irreducible p) :

Associates.count p (Associates.factors m) ≠ 0 → p ≤ m

source

theorem Associates.count_ne_zero_iff_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : α} {p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :

Associates.count (Associates.mk p) (Associates.factors (Associates.mk a)) ≠ 0 ↔ p ∣ a

source

theorem Associates.count_self {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {p : Associates α} (hp : Irreducible p) :

Associates.count p (Associates.factors p) = 1

source

theorem Associates.count_eq_zero_of_ne {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {p : Associates α} {q : Associates α} (hp : Irreducible p) (hq : Irreducible q) (h : p ≠ q) :

Associates.count p (Associates.factors q) = 0

source

theorem Associates.count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) :

Associates.count p (Associates.factors (a * b)) = Associates.count p (Associates.factors a) + Associates.count p (Associates.factors b)

source

theorem Associates.count_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {p : Associates α} (hp : Irreducible p) :

Associates.count p (Associates.factors a) = 0 ∨ Associates.count p (Associates.factors b) = 0

source

theorem Associates.count_mul_of_coprime {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) :

Associates.count p (Associates.factors a) = 0 ∨ Associates.count p (Associates.factors a) = Associates.count p (Associates.factors (a * b))

source

theorem Associates.count_mul_of_coprime' {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) :

Associates.count p (Associates.factors (a * b)) = Associates.count p (Associates.factors a) ∨ Associates.count p (Associates.factors (a * b)) = Associates.count p (Associates.factors b)

source

theorem Associates.dvd_count_of_dvd_count_mul {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {k : ℕ} (habk : k ∣ Associates.count p (Associates.factors (a * b))) :

k ∣ Associates.count p (Associates.factors a)

source

@[simp]

theorem Associates.factors_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] :

Associates.factors 1 = 0

source

@[simp]

theorem Associates.pow_factors {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} {k : ℕ} :

Associates.factors (a ^ k) = k • Associates.factors a

source

theorem Associates.count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) :

Associates.count p (Associates.factors (a ^ k)) = k * Associates.count p (Associates.factors a)

source

theorem Associates.dvd_count_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {p : Associates α} (hp : Irreducible p) (k : ℕ) :

k ∣ Associates.count p (Associates.factors (a ^ k))

source

theorem Associates.is_pow_of_dvd_count {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} (ha : a ≠ 0) {k : ℕ} (hk : ∀ (p : Associates α), Irreducible p → k ∣ Associates.count p (Associates.factors a)) :

∃ b, a = b ^ k

source

theorem Associates.eq_pow_count_factors_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {p : Associates α} {a : Associates α} (hp : Irreducible p) {n : ℕ} (h : a ∣ p ^ n) :

a = p ^ Associates.count p (Associates.factors a)

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).

source

theorem Associates.count_factors_eq_find_of_dvd_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) :

Nat.find (_ : ∃ n, (fun n => a ∣ p ^ n) n) = Associates.count p (Associates.factors a)

source

theorem Associates.eq_pow_of_mul_eq_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] [Nontrivial α] {a : Associates α} {b : Associates α} {c : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) {k : ℕ} (h : a * b = c ^ k) :

∃ d, a = d ^ k

source

theorem Associates.eq_pow_find_of_dvd_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [dec_irr : (p : Associates α) → Decidable (Irreducible p)] [UniqueFactorizationMonoid α] [dec : DecidableEq α] [dec' : DecidableEq (Associates α)] {a : Associates α} {p : Associates α} (hp : Irreducible p) [(n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n) :

a = p ^ Nat.find (_ : ∃ n, (fun n => a ∣ p ^ n) n)

The only divisors of prime powers are prime powers.

source

theorem Associates.quot_out {α : Type u_2} [CommMonoid α] (a : Associates α) :

Associates.mk (Quot.out a) = a

source

noncomputable def UniqueFactorizationMonoid.toGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq (Associates α)] [DecidableEq α] :

GCDMonoid α

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

source

noncomputable def UniqueFactorizationMonoid.toNormalizedGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq (Associates α)] [DecidableEq α] :

NormalizedGCDMonoid α

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

Equations

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

Instances For

source

noncomputable def UniqueFactorizationMonoid.fintypeSubtypeDvd {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Fintype Mˣ] (y : M) (hy : y ≠ 0) :

Fintype { x // 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

source

noncomputable def factorization {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] (n : α) :

α →₀ ℕ

This returns the multiset of irreducible factors as a Finsupp.

Equations

factorization n = ↑Multiset.toFinsupp (UniqueFactorizationMonoid.normalizedFactors n)

Instances For

source

theorem factorization_eq_count {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {n : α} {p : α} :

↑(factorization n) p = Multiset.count p (UniqueFactorizationMonoid.normalizedFactors n)

source

@[simp]

theorem factorization_zero {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] :

factorization 0 = 0

source

@[simp]

theorem factorization_one {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] :

factorization 1 = 0

source

@[simp]

theorem support_factorization {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {n : α} :

(factorization n).support = Multiset.toFinset (UniqueFactorizationMonoid.normalizedFactors n)

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

source

@[simp]

theorem factorization_mul {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {a : α} {b : α} (ha : a ≠ 0) (hb : b ≠ 0) :

factorization (a * b) = factorization a + factorization b

For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

source

theorem factorization_pow {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] {x : α} {n : ℕ} :

factorization (x ^ n) = n • factorization x

For any p, the power of p in x^n is n times the power in x

source

theorem associated_of_factorization_eq {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] [DecidableEq α] (a : α) (b : α) (ha : a ≠ 0) (hb : b ≠ 0) (h : factorization a = factorization b) :

Associated a b