nat.has_pow

Stream: general

[Johan Commelin]

⊢ nat.has_pow = monoid.has_pow

Meh

[Mario Carneiro]

there are lemmas about that, you unfolded too much

[Johan Commelin]

It's too bad it isn't defeq.

[Kevin Buzzard]

IIRC the products are different ways around! Is that right? One is a*a^n and one is a^n*a?

[Mario Carneiro]

that's true, but I think they wouldn't be defeq even if they were the same way around

[Mario Carneiro]

I'm not sure if there is some principled reason to prefer one over the other... I guess a * a^n matches list order

[Floris van Doorn]

For nat a^{n+1} ≡ a^n * a seems more natural. Since multiplication is defined by recursion on the second argument (succ a)^(succ n) is definitionally a successor. This is very minor, of course.