powers are monotone in the base

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I have been looking for the lemma below in mathlib (or something similar), but I could not find it. All the lemmas that I found with pow typically change the exponent, not the base. Is there a naming convention for referring to the exponent, rather than the base?

Thank you!

import algebra.algebra.basic

lemma pow_le_pow_of_base_le {R : Type*} [ordered_semiring R] {a b : R} {n : ℕ}
  (a0 : 0 ≤ a) (ab : a ≤ b) :
  a ^ n ≤ b ^ n :=
begin
  induction n with n hn,
  { rw [pow_zero, pow_zero] },
  { exact mul_le_mul ab hn (pow_nonneg a0 _) (a0.trans ab) }
end

[The import may not be minimal.]

[Heather Macbeth]

How about docs#pow_le_pow_of_le_left ?

[Damiano Testa]

Thanks Heather! This is exactly the lemma that I needed! I was convinced that I had library_searched as well...

And it turns out that I should have made n explicit! :smile:

[Kevin Buzzard]

Shouldn't this be called something like pow_mono or is that something else?

[Damiano Testa]

I think that there already is a pow_mono but it is on the exponent, rather than the base.

[Damiano Testa]

Until Heather's suggestion, I think that I had seen mostly lemmas with pow referring to the exp, instead of the base.