Theorems · Definition · commutative algebra
FiniteMultiplicity
{α : Type u_1} → [Monoid α] → α → α → PropFiniteMultiplicity a b indicates that the multiplicity of a in b is finite.
- Defined in
- Mathlib.RingTheory.Multiplicity
- Cited by
- 73 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by74
Results whose statement or proof uses this declaration.
- emultiplicityproof · cited by 156
- FiniteMultiplicity.emultiplicity_eq_multiplicitystatement and proof · cited by 31
- Nat.finiteMultiplicity_iffstatement · cited by 13
- emultiplicity_zeroproof · cited by 10
- emultiplicity_mulproof · cited by 10
- emultiplicity_eq_topstatement and proof · cited by 9
- emultiplicity_eq_zeroproof · cited by 8
- pow_dvd_of_le_emultiplicityproof · cited by 8
- Polynomial.rootMultiplicity_eq_multiplicityproof · cited by 8
- emultiplicity_le_emultiplicity_iffproof · cited by 7
- Polynomial.finiteMultiplicity_X_sub_Cstatement · cited by 7
- multiplicity_le_emultiplicityproof · cited by 5