Stream: Is there code for X?
Hallow World (Mar 26 2021 at 19:41):
Is there anything about the monotonicity of log on naturals? I have a branch with a proof and some additional lemmas not directly related (log_eq_zero) that help weaken some assumptions on nat.multiplicity.
Ruben Van de Velde (Mar 26 2021 at 19:44):
Seems like https://leanprover-community.github.io/mathlib_docs/data/nat/log.html#nat.log has all we know about about
Hallow World (Mar 26 2021 at 19:48):
Yeah that's where I was looking for and it seems awfully empty compared with powers. If there's nothing could I make a contribution? Username's: hallow-world
Kevin Buzzard (Mar 26 2021 at 19:51):
@maintainers could github user hallow-world have push access to non-master branches of mathlib?
I guess that this is in some sense a pretty unnatural function (but I trust that Simon wanted it for a good reason!) Number-theoretically the more interesting function is the number of times b goes into n. But the function is there so feel free to add to the API!
Bryan Gin-ge Chen (Mar 26 2021 at 19:52):
@Hallow World invite sent! https://github.com/leanprover-community/mathlib/invitations
Hallow World (Mar 26 2021 at 19:53):
Bryan Gin-ge Chen (Mar 26 2021 at 20:49):
Thanks for PR #6899!
Last updated: May 19 2021 at 02:10 UTC