Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors

∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] {a b : R},
  Irreducible a →
    b ≠ 0 → emultiplicity 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. 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 _) _..

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Cited by

14 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroUniqueFactorizationMonoidNormalizationMonoidDecidableEq