non-natural exponents?

Stream: maths

[Belisarius Cawl]

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]

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

[Johan Commelin]

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

[Johan Commelin]

docs#real.has_pow should work

[Johan Commelin]

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

[Belisarius Cawl]

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

[Belisarius Cawl]

works, woohoo!

[Belisarius Cawl]

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]

(n:ℝ) coerces an integer to a real

[Johan Commelin]

You can certainly just write n + m for integer addition

[Johan Commelin]

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

[Johan Commelin]

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

[Belisarius Cawl]

Yeah, I guess I tried to plus nats and wholes

[Belisarius Cawl]

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

[Belisarius Cawl]

(works)

[Kevin Buzzard]

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]

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