Commit 2025-07-05 06:23 b102252b

View on Github →

feat(WithZero): more lemmas about exp and log (#26761) These turned out useful in two separate PRs.

Estimated changes

added theorem WithZero.exp_ne_zero
added theorem WithZero.exp_lt_exp
added theorem WithZero.exp_pos
modified theorem WithZero.le_log_iff_exp_le
modified theorem WithZero.log_le_iff_le_exp
modified theorem WithZero.log_le_log
modified theorem WithZero.log_lt_iff_lt_exp
added theorem WithZero.log_lt_log
modified theorem WithZero.lt_log_iff_exp_lt