Zulip Chat Archive

Stream: Is there code for X?

Topic: int.iterate


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Ruben Van de Velde (Feb 20 2021 at 15:03):

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

view this post on Zulip 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?

view this post on Zulip Ariel Fridman (Feb 20 2021 at 15:06):

ah, nvm, looked through the file

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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