feat(data/nat/log): log_mul, log_div (#11164)
feat(data/nat/log): log_mul, log_div (#11164)

Even with division over natural, the log "spec" holds.



Co-authored-by: Yakov Pechersky <9925c0c20eafe10b1eaac37c5fe124dc0b28ca8c@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib