Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.log_mono


view this post on Zulip 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.

view this post on Zulip 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 nat.log

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Bryan Gin-ge Chen (Mar 26 2021 at 19:52):

@Hallow World invite sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Hallow World (Mar 26 2021 at 19:53):

Thanks!

view this post on Zulip Bryan Gin-ge Chen (Mar 26 2021 at 20:49):

Thanks for PR #6899!


Last updated: May 19 2021 at 02:10 UTC