Automorphism group of a cyclic group.

Stream: Is there code for X?

[Adam Topaz]

Suppose $G$ is finite cyclic of size $n$, leanified as IsCyclic G and Fintype G, for example. Do we have in mathlib the isomorphism between $Aut(G)$ and $(\mathbb{Z}/n)^\times$?

[Adam Topaz]

Do we have it for ZMod n?

[Jireh Loreaux]

I wrote this in a branch, let me find it. The problem is that it doesn't to_additiveize currently because Lean wants to apply it to $(\mathbb{Z}/n)^{\times}$

[Jireh Loreaux]

branch#j-loreaux/generator

[Adam Topaz]

Thanks!

[Jireh Loreaux]

Oh, actually, it's not quite what you asked for.

[Jireh Loreaux]

Nevermind. I have the bijection generators and the units of ZMod n.

[Jireh Loreaux]

However, that branch is probably quite useful for getting your hands on this isomorphism.

[Adam Topaz]

Aha I see.

[Adam Topaz]

Yes, still very helpful. Thanks!

[Jireh Loreaux]

Feel free to clean up that branch and PR it if you wish. I'm too busy with other things to focus on it.

[Adam Topaz]

I probably won't do anything with it since I found another more direct approach to what I was actually looking into.