Theorems · Theorem · commutative algebra

emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity

Deprecated since 2026-04-16Use Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity instead.

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {r d : R} (hr : r ≠ 0) (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r),
  emultiplicity d r = emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (Ideal.span {r})

Alias of Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity. The bijection normalizedFactorsEquivSpanNormalizedFactors between the set of prime factors of r and the set of prime factors of the ideal ⟨r⟩ preserves multiplicities. See count_normalizedFactorsSpan_eq_count for the version stated in terms of multisets count.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsPrincipalIdealRingNormalizationMonoid