ZMod to cyclic group

Stream: Is there code for X?

[Aaron Liu]

Given a group G generated by g, how can I get the obvious function from ZMod to G sending 1 to g?

import Mathlib

example {G : Type*} [Group G] {g : G} {n : ℕ} (hn : Nat.card G = n) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    { f : Multiplicative (ZMod n) ≃* G // ∀ i : ℤ, f (Multiplicative.ofAdd i) = g ^ i } :=
  sorry

[Snir Broshi]

docs#zmodCyclicMulEquiv ?

[Aaron Liu]

how do I know it sends 1 to g

[Violeta Hernández]

The proof of docs#zmodAddCyclicAddEquiv takes a generator using the axiom of choice so you could probably just make an alternate version which takes a generator, and reprove the other version using it.

[Edward van de Meent]

my solution:

lemma Multiplicative.ofAdd_zsmul {G : Type*} [AddGroup G] (z : ℤ) (g : G) :
  Multiplicative.ofAdd (z • g) = (Multiplicative.ofAdd g) ^ z := rfl

noncomputable example {G : Type*} [Group G] {g : G} {n : ℕ} (hn : Nat.card G = n) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    { f : Multiplicative (ZMod n) ≃* G // ∀ i : ℤ, f (Multiplicative.ofAdd i) = g ^ i } where
  val := by
    apply mulEquivOfOrderOfEq (g := Multiplicative.ofAdd 1) _ (g' := g) hg
    · simp only [orderOf_ofAdd_eq_addOrderOf, ZMod.addOrderOf_one, ← hn]
      symm
      exact orderOf_eq_card_of_forall_mem_zpowers hg
    · simp only [Subgroup.mem_zpowers_iff, Multiplicative.forall]
      simp_rw [← Multiplicative.ofAdd_zsmul]
      simp only [zsmul_eq_mul, mul_one, EmbeddingLike.apply_eq_iff_eq]
      change Function.Surjective _
      exact ZMod.intCast_surjective
  property := by
    intro i
    induction i with
    | zero => simp
    | succ i hi =>
      simpa [zpow_add] using hi
    | pred i hi =>
      simpa [zpow_sub,div_eq_mul_inv] using hi

[Aaron Liu]

Great! Do you think you can PR to mathlib?

[Edward van de Meent]

i'm not convinced that this is the right shape for mathlib, tbh. this is just a quick-and-dirty someone-needs-this-for-their-project write-once-and-forget solution

[Aaron Liu]

Oh, I need this for a proof I intend to PR to mathlib

[Edward van de Meent]

i bet there's people smarter than me who know a more idiomatic way to prove this... (please please do suggest improvements)

[Aaron Liu]

#34629

[Kim Morrison]

@Aaron Liu, do you think you could explain in doc-comments the link with the existing ones that use choice, and possibly update the doc-comments of the choiceful defs too?