# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: real.log_ne_zero_iff?

#### Ryan Lahfa (Feb 01 2021 at 15:23):

I feel this theorem is missing:

```
import analysis.special_functions.exp_log
lemma real.log_ne_zero_iff (x: ℝ) (hpos: 0 < x): (real.log x ≠ 0 ↔ x ≠ 1) := sorry
```

The closest thing to this is `log_pos`

which can help derive it, unsure if it is considered enough? (It seems like the situation is similar for the complex version of exponential)

#### Johan Commelin (Feb 01 2021 at 15:29):

Is it true? What is `real.log (-1)`

?

#### Ryan Lahfa (Feb 01 2021 at 15:31):

I should try to prove first :p but what I meant is:

```
lemma real.log_ne_zero_of_ne_one (x: ℝ) (hx_pos: 0 < x) (hx: x ≠ 1): real.log x ≠ 0 :=
begin
by_cases (1 < x),
exact ne_of_gt (real.log_pos h),
push_neg at h,
exact ne_of_lt (real.log_neg hx_pos (lt_of_le_of_ne h hx)),
end
```

#### Yakov Pechersky (Feb 01 2021 at 16:45):

Isn't this just injectivity of log?

#### Ryan Lahfa (Feb 01 2021 at 16:55):

Yakov Pechersky said:

Isn't this just injectivity of log?

I'm not sure I see a proof of the log injectivity in the file, though there is a proof that exp is injective in the same file

#### Mario Carneiro (Feb 01 2021 at 16:55):

injectivity of log is the same as functionality of exp

#### Ryan Lahfa (Feb 01 2021 at 16:55):

functionality := ?

#### Mario Carneiro (Feb 01 2021 at 16:56):

being a function

#### Mario Carneiro (Feb 01 2021 at 16:56):

exp is a function

#### Yakov Pechersky (Feb 01 2021 at 16:56):

`log x = y \iff x = exp y`

#### Ryan Lahfa (Feb 01 2021 at 16:56):

Ah, right

#### Mario Carneiro (Feb 01 2021 at 16:56):

of course, log isn't, really, since exp isn't injective

#### Ryan Lahfa (Feb 01 2021 at 16:56):

`log x = 0 iff x = exp 0 = 1`

, indeed.

#### Yakov Pechersky (Feb 01 2021 at 16:58):

`real.exp`

isn't injective?!

#### Yakov Pechersky (Feb 01 2021 at 16:59):

#### Mario Carneiro (Feb 01 2021 at 16:59):

ah, good point

#### Mario Carneiro (Feb 01 2021 at 16:59):

I was thinking of `complex.exp`

#### Yakov Pechersky (Feb 01 2021 at 17:00):

We have some missing lemmas relating the inverses of `real.log`

and `real.exp`

#### Yakov Pechersky (Feb 01 2021 at 17:01):

And then "injectivity" of `real.log`

comes out of having an inverse, etc.

#### Yury G. Kudryashov (Feb 02 2021 at 03:58):

Note that we have docs#real.strict_mono_incr_on_log

#### Yury G. Kudryashov (Feb 02 2021 at 04:00):

And docs#strict_mono_incr_on.inj_on

But a PR with `(h : x ≠ 0) : log x = y ↔ exp y = abs x`

and `(h : 0 < x) : log x = y ↔ exp y = x`

is very welcome.

#### Ryan Lahfa (Feb 02 2021 at 12:25):

Yury G. Kudryashov said:

And docs#strict_mono_incr_on.inj_on

But a PR with`(h : x ≠ 0) : log x = y ↔ exp y = abs x`

and`(h : 0 < x) : log x = y ↔ exp y = x`

is very welcome.

Alright, will try to come up with something

#### Ryan Lahfa (Feb 02 2021 at 12:25):

Thanks!

#### Eric Wieser (Feb 02 2021 at 12:29):

Is there a bundled `exp`

equiv from real to R+?

#### Yury G. Kudryashov (Feb 02 2021 at 13:23):

Last updated: May 07 2021 at 18:19 UTC