Exponantiating the Naturals

Stream: new members

[Lucas Teixeira]

Is there a function for exponantiating the naturals in MathLib??? I'm working through TPIL and ch.4 has us define a Fermat prime using data.nat.basic, but after reading the documentation I couldn't find anything.

[Kevin Buzzard]

What do you mean precisely? Just $a^b$ with a and b naturals? That should be a ^ b.

[Lucas Teixeira]

I keep getting the error

failed to synthesize type class instance for
n p n x y : ℕ
⊢ has_pow ℕ ℕ

[Reid Barton]

You should import something like algebra.group_power.