int.iterate

Stream: Is there code for X?

[Ariel Fridman]

I somehow found the group theory game, and looking through its files (specifically, the definition of power), and saw that it uses int.iterate, but I cant find such a method in the mathlib documentation, nor in my installation. Does this function actually exist, or is it made up for the game?

[Ariel Fridman]

The parts that matter:

import int.iterate

namespace mygroup

namespace group

variables {G : Type} [group G]

open int

/-- left multiplication is a bijection-/
def lmul (g : G) : G ≃ G :=
{ to_fun := (*) g, inv_fun := (*) g⁻¹,
  left_inv := begin intro x, rw [← mul_assoc, mul_left_inv, one_mul], end,
  right_inv := begin intro x, rw [← mul_assoc, mul_right_inv, one_mul] end }

def pow : G → ℤ → G :=
  λ g n, (iterate n (lmul g)) 1

[Ruben Van de Velde]

Part of the game: https://github.com/ImperialCollegeLondon/group-theory-game/blob/master/src/int/iterate.lean

[Ariel Fridman]

Ah, thank you! no idea how I missed that ^^'. This method seems useful though, is there a reason why we don't have something like that in matlib\stdlib?

[Ariel Fridman]

ah, nvm, looked through the file

[Ruben Van de Velde]

There's a couple of things that iterate with nats; I don't know if anyone's had a use case in mathlib for the int variant

[Kevin Buzzard]

Oh this was just one of the experiments we did. It's a total cheat IIRC because it uses Lean groups to make it, and then we use it to make our own group theory development.

[Kevin Buzzard]

OTOH I could totally imagine making an actual int.iterate independent of group theory, it's some kind of lambda calculus way of thinking about int I think, I forgot the details. The docs are a bit mangled in that file, I introduced a notation {{n}}^f for the n'th iterate of f because I wanted to experiment with the integer on the left, but I remember it drove Jason nuts and it looks like he deleted it :-) My logic was that there are problems with to_additive when it comes to pow v smul because g^n has n on the right and n \bub g has n on the left.