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.

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} [CancelCommMonoidWithZero α] [WfDvdMonoid α] {a b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) : FiniteMultiplicity a b

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

theorem UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors {R : Type u_2} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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.

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

theorem UniqueFactorizationMonoid.count_normalizedFactors_eq {R : Type u_2} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero 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.