multiplicity a b returns the largest natural number n such that
a ^ n ∣ b, as an enat or natural with infinity. If ∀ n, a ^ n ∣ b,
then it returns ⊤
multiplicity a b
a ^ n ∣ b
∀ n, a ^ n ∣ b
multiplicity.finite a b indicates that the multiplicity of a in b is finite.
multiplicity.finite a b