Theorems · Theorem · commutative algebra

Ideal.count_associates_factors_eq

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I J : Ideal R},
  I ≠ 0 →
    J.IsPrime →
      J ≠ ⊥ →
        (Associates.mk J).count (Associates.mk I).factors =
          Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)

The number of times an ideal I occurs as normalized factor of another ideal J is stable when regarding these ideals as associated elements of the monoid of ideals.

Defined in: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Cited by: 4 results in Mathlib
Foundations: Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDedekindDomain

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Idealstatement and proof · cited by 4,748
Bot.botstatement and proof · cited by 4,720
le_reflproof · cited by 2,061
Ideal.IsPrimestatement and proof · cited by 827
IsDedekindDomainstatement and proof · cited by 668
Irreducibleproof · cited by 496
Multiset.countstatement · cited by 302
Associatesproof · cited by 210
UniqueFactorizationMonoid.normalizedFactorsstatement · cited by 151
Associates.mkstatement and proof · cited by 137
Associates.factorsstatement and proof · cited by 97

Cited by4

Results whose statement or proof uses this declaration.

Ideal.count_associates_eqproof · cited by 2
IsDedekindDomain.HeightOneSpectrum.intValuation_eq_exp_neg_multiplicityproof · cited by 2
PowerSeries.intValuation_eq_of_coeproof · cited by 2
count_associates_factors_eqproof · cited by 0