## Stream: Is there code for X?

### Topic: int.iterate

#### Ariel Fridman (Feb 20 2021 at 15:01):

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 (Feb 20 2021 at 15:01):

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


#### Ariel Fridman (Feb 20 2021 at 15:05):

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 (Feb 20 2021 at 15:06):

ah, nvm, looked through the file

#### Ruben Van de Velde (Feb 20 2021 at 15:09):

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 (Feb 20 2021 at 17:06):

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 (Feb 20 2021 at 17:10):

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.

Last updated: May 17 2021 at 15:13 UTC