Zulip Chat Archive

Stream: new members

Topic: Integer powers


view this post on Zulip Ben Nale (Aug 10 2020 at 20:07):

Hi. image.png
I'm trying to prove lemmas that involve taking an integer to the power of an integer. However, I get the following error message. image.png

Please help. Thanks.

view this post on Zulip Thomas Browning (Aug 10 2020 at 20:12):

The problem is that lean doesn't know what (integer)^(integer) is. You might have to import something.

view this post on Zulip Reid Barton (Aug 10 2020 at 20:17):

What's 3 ^ (-7)?

view this post on Zulip Reid Barton (Aug 10 2020 at 20:17):

Exponents for int should be nats.

view this post on Zulip Thomas Browning (Aug 10 2020 at 20:18):

There is (real)^(integer) somewhere in mathlib (I think), so you could cast the base to the real numbers, and take the pow there.

view this post on Zulip Ben Nale (Aug 10 2020 at 20:18):

image.png
I get the same error

view this post on Zulip Ben Nale (Aug 10 2020 at 20:20):

image.png
image.png

view this post on Zulip Reid Barton (Aug 10 2020 at 20:20):

What would you expect to get?

view this post on Zulip Reid Barton (Aug 10 2020 at 20:21):

a^b always has the same type as a

view this post on Zulip Alex J. Best (Aug 10 2020 at 20:21):

Ben Nale said:

image.png
image.png

In this the left hand side is a nat and the right hand side is an int.

view this post on Zulip Ben Nale (Aug 10 2020 at 20:22):

hmm. but naturals are a subset of ints. How do I tell that to lean?

view this post on Zulip Alex J. Best (Aug 10 2020 at 20:23):

You can explicitly write : int or : \Z as you did on the right hand side.

view this post on Zulip Alex J. Best (Aug 10 2020 at 20:23):

That will make -1 as an  int

view this post on Zulip Ben Nale (Aug 10 2020 at 20:24):

oh nice :). That works. I understand now. Thank you very much @Alex J. Best @Reid Barton

view this post on Zulip Patrick Massot (Aug 10 2020 at 20:25):

Note for next time: copy-pasting text is almost always better than posting screenshots. See also this link: #mwe.


Last updated: May 14 2021 at 22:15 UTC