## Stream: Is there code for X?

### Topic: powers are monotone in the base

#### Damiano Testa (Feb 10 2021 at 05:19):

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.]

#### Damiano Testa (Feb 10 2021 at 06:17):

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 (Feb 10 2021 at 06:40):

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

#### Damiano Testa (Feb 10 2021 at 06:41):

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

#### Damiano Testa (Feb 10 2021 at 06:42):

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

Last updated: May 17 2021 at 16:26 UTC