Theorems · Theorem · commutative algebra
count_associates_factors_eq
Deprecated since 2026-04-16Use Ideal.count_associates_factors_eq instead.
∀ {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)Alias of Ideal.count_associates_factors_eq.
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.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIsDedekindDomain
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement · cited by 17,173
- Idealstatement · cited by 4,748
- Bot.botstatement · cited by 4,720
- Ideal.IsPrimestatement · cited by 827
- IsDedekindDomainstatement · cited by 668
- Multiset.countstatement · cited by 302
- UniqueFactorizationMonoid.normalizedFactorsstatement · cited by 151
- Associates.mkstatement · cited by 137
- Associates.factorsstatement · cited by 97
- Associates.countstatement · cited by 79
- Ideal.count_associates_factors_eqproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.