list.rotate

Stream: general

[Bolton Bailey]

It seems we have a list.rotate to rotate a list to the left by a certain number, I might like to fill out the API by making a function to rotate to the right, or also rotate by an arbitrary integer. How should I go about this?

[Bolton Bailey]

/poll <Rotate options>
Don't change anything
Change list.rotate to take an integer, refactor other appearances to use this
Make three functions named rotate, rotate_left, rotate_right
Make three functions named rotate_int, rotate, rotate_right
Make three functions named rotate, rotatel, rotater

[Yaël Dillies]

Probably a bad idea, but you could go so far as declaring a mul_action int (list a) instance!

[Eric Rodriguez]

do we have a mul_action a $ list a instance?

[Eric Rodriguez]

I feel like it'd be weird because the more natural smul instance is the nat instance, and I know those can coexist but imagine seeing 2 smul l in the infoview and not knowing which it was

[Eric Wieser]

Since when was rotating by 1 the identity @Yaël Dillies?

[Kevin Buzzard]

What about mul_action (multiplicative int) (list a) then? Given that multiplicative int seems to be the canonical infinite cyclic group in mathlib...

[Kevin Buzzard]

Or add_action int (list a) which I (edit: incorrectly) presume doesn't exist

[Eric Wieser]

docs#add_action would work fine, but I don't think it's a particularly sensible use of the typeclass here; not every α →+ additive (End β) is canonical enough to get a typeclass instance

[Yaël Dillies]

Yes sorry I meant add_action indeed!

[Chris Hughes]

Yaël Dillies said:

Probably a bad idea, but you could go so far as declaring a mul_action int (list a) instance!

I think this is why I introduced list.rotate. It was something to do with Sylow theorems.

[Kevin Buzzard]

For Sylow you need an element of order p in a group whose order is a multiple of p to start the induction off, and one way to get it is by looking at all lists of length p the product of whose elements is 1 and then observing that rotation must have at least p fixed points because it has one fixed point and the number is congruent to 0 mod p