Zulip Chat Archive

Stream: general

Topic: iterate


view this post on Zulip Johan Commelin (May 11 2020 at 04:43):

Should function.iterate be replaced by a has_pow instance? For example by making X → X a monoid?

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 04:54):

I think that for most people f * g means pointwise multiplication.

view this post on Zulip Kenny Lau (May 11 2020 at 05:36):

that is correct in Lean with algebra/pi_instances

view this post on Zulip Johan Commelin (May 11 2020 at 05:40):

Yury G. Kudryashov said:

I think that for most people f * g means pointwise multiplication.

Fair enough

view this post on Zulip Mario Carneiro (May 11 2020 at 05:49):

There is the perm group, but I don't know if we have endo X for this

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 05:50):

End X

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 05:50):

From category theory.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 06:17):

But often it's convenient to iterate without using a type tag.

view this post on Zulip Mario Carneiro (May 11 2020 at 06:34):

that's why ^[n] is a special notation

view this post on Zulip Johan Commelin (May 11 2020 at 06:35):

But it could be notation for has_pow wrt a monoid that is not an instance?

view this post on Zulip Johan Commelin (May 11 2020 at 06:35):

Anyway, that sounds like more refactoring trouble than it's worth


Last updated: May 17 2021 at 22:15 UTC