Zulip Chat Archive

Stream: new members

Topic: Lemma for removing exponents from both sides?


Belisarius Cawl (Mar 26 2021 at 07:00):

I can't find a lemma which says

(a b c :  ) (ha : a >0) (hb : b > 0) (hc : c  0) : a = b  a^c = b^c

EDIT
and similar stuff for exponents. Looking at https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/pow.html

Scott Morrison (Mar 26 2021 at 07:07):

(deleted)

Hanting Zhang (Mar 26 2021 at 07:08):

Don't think it exists; however there is docs#real.rpow_le_rpow_iff, and you can get your result by applying it twice.

Scott Morrison (Mar 26 2021 at 07:09):

Should be added if it's not there. A good easy PR! (Do write ha : 0 < a, however, reverse the iff, and make it a @[simp] lemma!)

Johan Commelin (Mar 26 2021 at 07:10):

We should prove it's a strict_mono

Belisarius Cawl (Mar 26 2021 at 07:10):

Was thinking the same. Thank you two!

Belisarius Cawl (Mar 26 2021 at 07:21):

@Hanting Zhang this seems not so straightforward though, since in my lemma the exponent can be negative.

Johan Commelin (Mar 26 2021 at 07:24):

So you have to case split on the sign of c

Johan Commelin (Mar 26 2021 at 07:25):

Hopefully there is docs#real.rpow_le_rpow_iff_of_neg

Belisarius Cawl (Mar 26 2021 at 07:25):

@Johan Commelin 404 Not Found :/

Johan Commelin (Mar 26 2021 at 07:26):

Yes, I noticed :sad:

Sebastien Gouezel (Mar 26 2021 at 07:41):

I gave exactly this lemma as part of my answer to your previous question, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/fastest.20approach.20to.20proving.20equation.20iffs/near/231864539

Scott Morrison (Mar 26 2021 at 07:44):

Hmmm...

Belisarius Cawl (Mar 26 2021 at 07:45):

Ah, did not see that. Still figuring out Zulip. Thanks a lot!


Last updated: Dec 20 2023 at 11:08 UTC