Theorems · Definition · commutative algebra
multiplicity
{α : Type u_1} → [Monoid α] → α → α → ℕA ℕ-valued version of emultiplicity, returning 1 instead of ⊤.
- Defined in
- Mathlib.RingTheory.Multiplicity
- Cited by
- 117 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 168 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- emultiplicityproof · cited by 156
- WithTop.untopDproof · cited by 33
Cited by118
Results whose statement or proof uses this declaration.
- FiniteMultiplicity.emultiplicity_eq_multiplicitystatement · cited by 31
- multiplicity_eq_of_emultiplicity_eq_somestatement · cited by 11
- emultiplicity_mulproof · cited by 10
- multiplicity_eq_of_emultiplicity_eqstatement · cited by 8
- Polynomial.rootMultiplicity_eq_multiplicitystatement · cited by 8
- pow_multiplicity_dvdstatement · cited by 7
- padicValNat_def'statement · cited by 6
- FiniteMultiplicity.not_pow_dvd_of_multiplicity_ltstatement and proof · cited by 5
- padicValRat.mulproof · cited by 5
- multiplicity_le_emultiplicitystatement and proof · cited by 5
- multiplicity_mulstatement and proof · cited by 5
- IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_oneproof · cited by 4