Zulip Chat Archive

Stream: Is there code for X?

Topic: nat.pow_pos


view this post on Zulip Ruben Van de Velde (Sep 15 2020 at 19:14):

Is there a reason to have both of these?

theorem nat.pos_pow_of_pos {b : } (n : ) : 0 < b  0 < b ^ n
theorem nat.pow_pos {p : } (hp : 0 < p) (n : ) : 0 < p ^ n

and do we not have

lemma nat.pos_pow_iff {b : } (n : ) (h : 0 < n) : 0 < b  0 < b ^ n

at all?

view this post on Zulip Johan Commelin (Sep 15 2020 at 19:21):

Just historical accidents... Note that it is likely better to swap the sides of the pos_pow_iff statement.
Feel free to PR.

view this post on Zulip Rob Lewis (Sep 15 2020 at 19:21):

0^0 = 1, no?

view this post on Zulip Ruben Van de Velde (Sep 15 2020 at 19:22):

Hence the 0 < n hypothesis, yeah

view this post on Zulip Rob Lewis (Sep 15 2020 at 19:23):

Oh, duh.


Last updated: May 16 2021 at 05:21 UTC