Commit 2022-12-06 20:53 dc9db541

feat(data/nat/log): review/extend API (#17809)

• Add nat.lt_mul_self_iff.
• Mark nat.log_eq_zero_iff as @[simp].
• Add a @[simp] lemma nat.log_pos_iff.
• Assume ≠ 0 instead of 0 < in nat.pow_le_iff_le_log and nat.lt_pow_iff_log_lt, add implications with weaker assumptions:
  • nat.le_log_of_pow_le,
  • nat.log_lt_of_lt_pow,
  • nat.lt_pow_of_log_lt,
  • nat.pow_le_of_le_log.
• Add nat.log_eq_iff and nat.log_eq_of_pow_le_of_lt_pow.
• Assume n ≠ 0 instead of 0 < n in nat.log_mul_base, use implicit arguments.
• Add nat.log_eq_iff and nat.log_eq_of_pow_le_of_lt_pow.
• Add nat.log_eq_one_iff', a version of log_eq_one_iff with seemingly weaker RHS.
• Drop assumption 1 < b in nat.pow_log_le_self.