power function injective over nat

Stream: new members

[Ainsley Pahljina]

This isn't in math lib, is there any chance someone can help me prove it?

lemma pow_inj (a b c : ℕ) (h : 2 ≤ a) : a^b = a^c → b = c := sorry

Thanks in advance!

[Bhavik Mehta]

I needed this same lemma too! My proof is here, but if you want hints rather than a solution, I'd suggest proving that pow is monotonic, and using that.

[Bhavik Mehta]

Useful library functions you might need include: pow_lt_pow_of_lt_right, le_antisymm, and other easy things about linear orders such as not_le_of_lt

[Bhavik Mehta]

Actually, monotonic was the wrong word to use, I'm suggesting you first prove

example { a b c : ℕ } ( h : 2 ≤ a ) ( k : a^b ≤ a^c ) : b ≤ c

[Kevin Buzzard]

Avoid \ge as a rule -- rewrite using \le

[Bhavik Mehta]

Edited, thanks

[Bhavik Mehta]

Is \ge just sugar over \le?

[Johan Commelin]

Most of the time: yes, but some parts of Lean are sensitive to the sugar

[Scott Morrison]

@Ainsley Pahljina or @Bhavik Mehta, it would be great to PR this to mathlib!

[Bhavik Mehta]

I'll try to make this PR later today!

[Bhavik Mehta]

@Scott Morrison Where would this sort of thing belong? In data/nat/basic.lean, maybe?

[Scott Morrison]

Yes.

[Bhavik Mehta]

@Scott Morrison PR here: https://github.com/leanprover-community/mathlib/pull/1683