Theorems · Definition · commutative algebra
Associates.count
{α : Type u_1} →
[inst : CommMonoidWithZero α] →
[DecidableEq (Associates α)] →
[(p : Associates α) → Decidable (Irreducible p)] → Associates α → Associates.FactorSet α → ℕcount p s is the multiplicity of the irreducible p in the FactorSet s.
If p is not irreducible, count p s is defined to be 0.
- Cited by
- 79 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommMonoidWithZerostatement and proof · cited by 913
- Irreduciblestatement and proof · cited by 496
- Associatesstatement and proof · cited by 210
- Associates.FactorSetstatement · cited by 52
- Associates.bcountproof · cited by 6
Cited by83
Results whose statement or proof uses this declaration.
- FractionalIdeal.countproof · cited by 25
- IsDedekindDomain.HeightOneSpectrum.maxPowDividingproof · cited by 17
- IsDedekindDomain.HeightOneSpectrum.intValuation_if_negstatement · cited by 11
- Associates.count.congr_simpstatement and proof · cited by 10
- IsDedekindDomain.HeightOneSpectrum.intValuationDefproof · cited by 9
- IsDedekindDomain.HeightOneSpectrum.intValuation_le_oneproof · cited by 9
- Associates.count_somestatement · cited by 8
- Ideal.hasFiniteMulSupportproof · cited by 7
- Associates.prime_pow_dvd_iff_lestatement · cited by 7
- Associates.count_mulstatement and proof · cited by 7
- Ideal.finprod_heightOneSpectrum_factorizationproof · cited by 6
- IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvdproof · cited by 5