Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.count_normalizedFactors_eq

∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {p x : R},
  Irreducible p →
    normalize p = p →
      ∀ {n : ℕ}, p ^ n ∣ x → ¬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.

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroUniqueFactorizationMonoidNormalizationMonoidDecidableEq