Zulip Chat Archive

Stream: new members

Topic: Integer powers


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.

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.

Reid Barton (Aug 10 2020 at 20:17):

What's 3 ^ (-7)?

Reid Barton (Aug 10 2020 at 20:17):

Exponents for int should be nats.

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.

Ben Nale (Aug 10 2020 at 20:18):

image.png
I get the same error

Ben Nale (Aug 10 2020 at 20:20):

image.png
image.png

Reid Barton (Aug 10 2020 at 20:20):

What would you expect to get?

Reid Barton (Aug 10 2020 at 20:21):

a^b always has the same type as a

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.

Ben Nale (Aug 10 2020 at 20:22):

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

Alex J. Best (Aug 10 2020 at 20:23):

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

Alex J. Best (Aug 10 2020 at 20:23):

That will make -1 as an  int

Ben Nale (Aug 10 2020 at 20:24):

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

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: Dec 20 2023 at 11:08 UTC