mathlib3

152412ff - feat(analysis/special_functions/exp_log): log_nonzero_of_ne_one and log_inj_pos (#6734)

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) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>