Zulip Chat Archive

Stream: Is there code for X?

Topic: even powers


view this post on Zulip Benjamin Davidson (Jan 20 2021 at 20:13):

Is there a lemma that states that any real number raised to an even natural power is nonnegative?

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:25):

I don't think so. The proof should be a 1-liner (maybe 2), but the lemma itself isn't there yet I think

view this post on Zulip Benjamin Davidson (Jan 20 2021 at 20:31):

Would that be via pow_bit0_nonneg? That's the only thing I came across that seems to relate to this.

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:32):

ooh, that might do it.

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:32):

I would have extracted n = 2 * k, and then rewrite to (x ^ k) ^ 2 and use pow_two_nonneg

view this post on Zulip Johan Commelin (Jan 20 2021 at 20:33):

but your version might be a step shorter

view this post on Zulip Benjamin Davidson (Jan 20 2021 at 20:36):

Oh that's clever as well! I'll try with pow_bit0_nonneg since the more I look at it the simpler it seems, but either way should be pretty easy. Cheers!


Last updated: May 16 2021 at 05:21 UTC