Theorems · Theorem · commutative algebra
emultiplicity_zero
∀ {α : Type u_1} [inst : MonoidWithZero α] (a : α), emultiplicity a 0 = ⊤- Defined in
- Mathlib.RingTheory.Multiplicity
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- ENatstatement · cited by 4,985
- MonoidWithZerostatement and proof · cited by 456
- emultiplicitystatement · cited by 156
- FiniteMultiplicityproof · cited by 73
- emultiplicity_eq_topproof · cited by 9
- FiniteMultiplicity.ne_zeroproof · cited by 3
Cited by10
Results whose statement or proof uses this declaration.
- Int.emultiplicity_pow_sub_powproof · cited by 2
- emultiplicity_prime_le_emultiplicity_image_by_factor_orderIsoproof · cited by 1
- Ideal.emultiplicity_botproof · cited by 1
- Nat.emultiplicity_pow_sub_powproof · cited by 1
- Nat.two_pow_sub_powproof · cited by 1
- Nat.Prime.emultiplicity_le_emultiplicity_choose_addproof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.emultiplicity_iSupproof · cited by 1
- Int.two_pow_sub_pow'proof · cited by 1
- Nat.toNat_emultiplicityproof · cited by 0
- PowerSeries.order_eq_emultiplicity_Xproof · cited by 0