## Stream: general

### Topic: nat.has_pow

#### Johan Commelin (May 16 2019 at 11:08):

⊢ nat.has_pow = monoid.has_pow


Meh

#### Mario Carneiro (May 16 2019 at 11:14):

there are lemmas about that, you unfolded too much

#### Johan Commelin (May 16 2019 at 13:13):

It's too bad it isn't defeq.

#### Kevin Buzzard (May 16 2019 at 13:59):

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

#### Mario Carneiro (May 16 2019 at 14:03):

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

#### Mario Carneiro (May 16 2019 at 14:04):

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 (May 16 2019 at 18:38):

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.

Last updated: May 13 2021 at 06:15 UTC