## Stream: general

### Topic: iterate

#### 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?

#### Yury G. Kudryashov (May 11 2020 at 04:54):

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

#### Kenny Lau (May 11 2020 at 05:36):

that is correct in Lean with algebra/pi_instances

#### 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

#### 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

#### Yury G. Kudryashov (May 11 2020 at 05:50):

End X

#### Yury G. Kudryashov (May 11 2020 at 05:50):

From category theory.

#### Yury G. Kudryashov (May 11 2020 at 06:17):

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

#### Mario Carneiro (May 11 2020 at 06:34):

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

#### Johan Commelin (May 11 2020 at 06:35):

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

#### 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