Theorems · Theorem · commutative algebra
Associates.count_some
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)]
[inst_2 : (p : Associates α) → Decidable (Irreducible p)] {p : Associates α} (hp : Irreducible p)
(s : Multiset { a // Irreducible a }), p.count ↑s = Multiset.count ⟨p, hp⟩ s- Cited by
- 8 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- WithTop.somestatement and proof · cited by 1,128
- CommMonoidWithZerostatement and proof · cited by 913
- Irreduciblestatement and proof · cited by 496
- Multiset.countstatement and proof · cited by 302
- Associatesstatement and proof · cited by 210
- Associates.countstatement · cited by 79
- Associates.FactorSetproof · cited by 52
- Associates.bcountproof · cited by 6
Cited by8
Results whose statement or proof uses this declaration.
- Associates.count_mulproof · cited by 7
- Associates.count_selfproof · cited by 4
- IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_countproof · cited by 2
- FractionalIdeal.count_maximal_coprimeproof · cited by 2
- IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_oneproof · cited by 1
- Associates.count_le_count_of_factors_leproof · cited by 1
- Associates.eq_factors_of_eq_countsproof · cited by 1
- Associates.is_pow_of_dvd_countproof · cited by 1