## 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

#### 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

#### 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:

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: May 14 2021 at 22:15 UTC