Commit 2021-08-28 08:03 8ee05e9a
View on Github →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.