Lemma for removing exponents from both sides?

Stream: new members

[Belisarius Cawl]

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]

(deleted)

[Hanting Zhang]

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]

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]

We should prove it's a strict_mono

[Belisarius Cawl]

Was thinking the same. Thank you two!

[Belisarius Cawl]

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

[Johan Commelin]

So you have to case split on the sign of c

[Johan Commelin]

Hopefully there is docs#real.rpow_le_rpow_iff_of_neg

[Belisarius Cawl]

@Johan Commelin 404 Not Found :/

[Johan Commelin]

Yes, I noticed :sad:

[Sebastien Gouezel]

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]

Hmmm...

[Belisarius Cawl]

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