Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-27 06:35 d32f9c72

View on Github →

feat(data/nat/log): add some lemmas and monotonicity (#6899)

Estimated changes

added theorem nat.log_b_one_eq_zero
added theorem nat.log_b_zero_eq_zero
added theorem nat.log_eq_zero
added theorem nat.log_eq_zero_of_le
added theorem nat.log_eq_zero_of_lt
added theorem nat.log_le_log_of_le
added theorem nat.log_le_log_succ
added theorem nat.log_mono
added theorem nat.log_one_eq_zero
added theorem nat.log_zero_eq_zero