# Zulip Chat Archive

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

#### Heather Macbeth (Feb 10 2021 at 05:49):

How about docs#pow_le_pow_of_le_left ?

#### 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