Zulip Chat Archive

Stream: general

Topic: nat.has_pow


view this post on Zulip Johan Commelin (May 16 2019 at 11:08):

 nat.has_pow = monoid.has_pow

Meh

view this post on Zulip Mario Carneiro (May 16 2019 at 11:14):

there are lemmas about that, you unfolded too much

view this post on Zulip Johan Commelin (May 16 2019 at 13:13):

It's too bad it isn't defeq.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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