mathlib

8ee05e9a - feat(data/nat/log): Ceil log (#8764)

feat(data/nat/log): Ceil log (#8764) Defines the upper natural log, which is the least `k` such that `n ≤ b^k`. Also expand greatly the docs of `data.nat.multiplicity`, in particular to underline that it proves Legendre's theorem.