iterate

Stream: general

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Kenny Lau]

that is correct in Lean with algebra/pi_instances

[Johan Commelin]

Yury G. Kudryashov said:

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

Fair enough

[Mario Carneiro]

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

[Yury G. Kudryashov]

End X

[Yury G. Kudryashov]

From category theory.

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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