Zulip Chat Archive

Stream: Is there code for X?

Topic: powers are monotone in the base


view this post on Zulip 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.]

view this post on Zulip Heather Macbeth (Feb 10 2021 at 05:49):

How about docs#pow_le_pow_of_le_left ?

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 06:40):

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

view this post on Zulip 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.

view this post on Zulip 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