nat.log_mono

Stream: Is there code for X?

[Hallow World]

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]

Seems like https://leanprover-community.github.io/mathlib_docs/data/nat/log.html#nat.log has all we know about about nat.log

[Hallow World]

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]

@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]

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

[Hallow World]

Thanks!

[Bryan Gin-ge Chen]

Thanks for PR #6899!