## Stream: maths

### Topic: non-natural exponents?

#### Belisarius Cawl (Mar 24 2021 at 10:46):

Hi all, apologies if I am misusing this. Tried the search unsuccessfully at least.

Am just getting started with LEAN, played the numbers game and read through the docs. Now for my own application I have equations with real exponents, but for anything other than natural exponents it says "failed to synthesize type class instance for [...] [base number type] ℝ" (stuff in brackets is mine).

What am I doing wrong? Any help would be greatly appreciated, learning curve's steep.

#### Johan Commelin (Mar 24 2021 at 10:47):

@Belisarius Cawl What did you import at the top of your file?

#### Johan Commelin (Mar 24 2021 at 10:47):

Also "equations" of what? You can't take real exponents of arbitrary things. They have to be something like real numbers.

#### Johan Commelin (Mar 24 2021 at 10:47):

docs#real.has_pow should work

#### Johan Commelin (Mar 24 2021 at 10:49):

So if you import analysis.special_functions.pow then you should be able to take real exps of real numbers

#### Belisarius Cawl (Mar 24 2021 at 10:49):

hey cool, will try it out right away. thanks a lot!

works, woohoo!

#### Belisarius Cawl (Mar 24 2021 at 11:00):

wait a second... This is very strange. Depending on whether the first occurence of exponentiation im my equation is real^real or whole^real, respectively, the other occurences of whole^real don't cause an error or do cause one. (At least until further down at another equation).

In any case I guess I have to convert my wholes to reals, no? How would I do that? In the docs (https://leanprover-community.github.io/mathlib_docs/data/real/basic.html#real) I don't see anything analogous to int.from_nat or however it's called.

As a related question - is it possible to add whole numbers with the "+" infix notation? LEAN complains until I use int.add.
(EDIT: only complains when I add wholes to nats which I guess is okay)

Again apologies for the messy noob questions, if you would like to point out a suggested way to deal with those myself I'd be happy to do so.

#### Johan Commelin (Mar 24 2021 at 11:04):

(n:ℝ) coerces an integer to a real

#### Johan Commelin (Mar 24 2021 at 11:05):

You can certainly just write n + m for integer addition

#### Johan Commelin (Mar 24 2021 at 11:05):

If that doesn't work, you've messed something up, somewhere

#### Johan Commelin (Mar 24 2021 at 11:05):

But we can't tell if you don't show us your code

#### Belisarius Cawl (Mar 24 2021 at 11:05):

Yeah, I guess I tried to plus nats and wholes

#### Belisarius Cawl (Mar 24 2021 at 11:06):

ok sure, wanted to avoid walls of text. will try what you said now first. Thanks!

(works)

#### Kevin Buzzard (Mar 24 2021 at 11:46):

You can only add numbers of the same type. If lean sees a + b then it assumes you're adding things of a's type and if b isn't of a's type then it will try to coerce it into a's type. So real + nat will work but nat + real won't.

#### Kevin Buzzard (Mar 24 2021 at 11:47):

For nat + real you need to coerce the nat yourself with (n : real)

Last updated: May 12 2021 at 07:17 UTC