Unique factorization and multiplicity

Main results

• UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors: The multiplicity of an irreducible factor of a nonzero element is exactly the number of times the normalized factor occurs in the normalizedFactors.

• UniqueFactorizationMonoid.dvd_iff_multiplicity_le: A nonzero element divides a nonzero element iff its multiplicity at every prime is at most that of the other.

• UniqueFactorizationMonoid.associated_iff_multiplicity_eq: Two nonzero elements are associated iff they have the same multiplicity at every prime.

theorem WfDvdMonoid.max_power_factor' {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α} (h : a₀ ≠ 0) (hx : ¬IsUnit x) : ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

theorem WfDvdMonoid.max_power_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α} (h : a₀ ≠ 0) (hx : Irreducible x) : ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

theorem FiniteMultiplicity.of_not_isUnit {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] {a b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) : FiniteMultiplicity a b

theorem FiniteMultiplicity.of_prime_left {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] {a b : α} (ha : Prime a) (hb : b ≠ 0) : FiniteMultiplicity a b

theorem Prime.finiteMultiplicity_iff_ne_zero {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] {a p : α} (hp : Prime p) : FiniteMultiplicity p a ↔ a ≠ 0

An element of a WfDvdMonoid has finite multiplicity at a prime iff it is nonzero.

theorem UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] {a b : R} {n : ℕ} (ha : Irreducible a) (hb : b ≠ 0) : ↑n ≤ emultiplicity a b ↔ Multiset.replicate n (normalize a) ≤ normalizedFactors b

theorem UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {a b : R} (ha : Irreducible a) (hb : b ≠ 0) : emultiplicity a b = ↑(Multiset.count (normalize a) (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.

For a version using multiplicity, see multiplicity_eq_count_normalizedFactors.

See also count_normalizedFactors_eq which expands the definition of multiplicity to produce a specification for count (normalizedFactors _) _..

theorem UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {a b : R} (ha : Irreducible a) (hb : b ≠ 0) : multiplicity a b = Multiset.count (normalize a) (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.

For a version using emultiplicity, see emultiplicity_eq_count_normalizedFactors.

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p x : R} (hp : Irreducible p) (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) : Multiset.count p (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.

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq' {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p x : R} (hp : p = 0 ∨ Irreducible p) (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) : Multiset.count p (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.

theorem UniqueFactorizationMonoid.associated_finprod_pow_count {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {x : R} (hx : x ≠ 0) : Associated (∏ᶠ (p : R), p ^ Multiset.count p (normalizedFactors x)) x

theorem UniqueFactorizationMonoid.finprod_pow_count_eq_of_subsingleton_units {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] [Subsingleton Rˣ] {x : R} (hx : x ≠ 0) : ∏ᶠ (p : R), p ^ Multiset.count p (normalizedFactors x) = x

theorem UniqueFactorizationMonoid.dvd_iff_emultiplicity_le {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) : a ∣ b ↔ ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b

theorem UniqueFactorizationMonoid.dvd_iff_multiplicity_le {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) (hb : b ≠ 0) : a ∣ b ↔ ∀ (p : R), Prime p → multiplicity p a ≤ multiplicity p b

A nonzero element of a UniqueFactorizationMonoid divides a nonzero element iff its multiplicity at every prime is at most that of the other.

theorem UniqueFactorizationMonoid.associated_iff_multiplicity_eq {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) (hb : b ≠ 0) : Associated a b ↔ ∀ (p : R), Prime p → multiplicity p a = multiplicity p b

Two nonzero elements of a UniqueFactorizationMonoid are associated iff they have the same multiplicity at every prime.

theorem UniqueFactorizationMonoid.pow_dvd_pow_iff_dvd {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} {n : ℕ} (hn : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b

theorem UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {α : Type u_3} {M : Type u_4} [CommMonoid M] [Subsingleton Rˣ] (f : α → M) {g : α → R} (hgi : Function.Injective g) (hg : ∀ (s : α), Irreducible (g s)) {r : R} (hr : r ≠ 0) : Function.HasFiniteMulSupport fun (s : α) => f s ^ multiplicity (g s) r