Theorems · Definition · commutative algebra

emultiplicity

{α : Type u_1} → [Monoid α] → α → α → ℕ∞

emultiplicity a b returns the largest natural number n such that a ^ n ∣ b, as an ℕ∞. If ∀ n, a ^ n ∣ b then it returns ⊤.

Defined in

Mathlib.RingTheory.Multiplicity

Cited by

156 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 162 definitions · uses propext, Classical.choice, Quot.sound

Assumes

Monoid