Zulip Chat Archive

Stream: general

Topic: nat.has_pow

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

 nat.has_pow = monoid.has_pow


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: Aug 03 2023 at 10:10 UTC