Integer powers

Stream: new members

[Ben Nale]

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]

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

[Reid Barton]

What's 3 ^ (-7)?

[Reid Barton]

Exponents for int should be nats.

[Thomas Browning]

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]

image.png
I get the same error

[Ben Nale]

image.png
image.png

[Reid Barton]

What would you expect to get?

[Reid Barton]

a^b always has the same type as a

[Alex J. Best]

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]

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

[Alex J. Best]

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

[Alex J. Best]

That will make -1 as an  int

[Ben Nale]

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

[Patrick Massot]

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