Zulip Chat Archive

Stream: new members

Topic: Exponantiating the Naturals


Lucas Teixeira (Sep 08 2021 at 18:21):

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 (Sep 08 2021 at 18:22):

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

Lucas Teixeira (Sep 08 2021 at 19:07):

I keep getting the error

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

Reid Barton (Sep 08 2021 at 19:08):

You should import something like algebra.group_power.


Last updated: Dec 20 2023 at 11:08 UTC