Commit 2021-03-19 17:15 152412ff

feat(analysis/special_functions/exp_log): log_nonzero_of_ne_one and log_inj_pos (#6734) log_nonzero_of_ne_one and log_inj_pos Proves :

• When x > 0, log(x) is 0 iff x = 1
• The real logarithm is injective (when restraining the domain to the positive reals)