pow_cancel_left

Stream: Is there code for X?

[Patrick Johnson]

Do we have something like this:

lemma pow_cancel_left {a b c : ℕ}
  (h₁ : 1 < c)
  (h₂ : c ^ a = c ^ b) :
  a = b

I have a very ugly proof, but I'm surprised I can't find any similar lemma in mathlib.

[Yaël Dillies]

Untested

lemma pow_cancel_left {a b c : ℕ} (h₁ : 1 < c) (h₂ : c ^ a = c ^ b) : a = b :=
(strict_mono_pow h₁).injective h₂

[Yaël Dillies]

This proof works for c in an ordered semiring, but the lemma should hold more generally.

[Patrick Johnson]

I totally forgot about strict_mono_pow. Thanks.