Equivalence between subgroup of multiples with with integers

Stream: Is there code for X?

[Bhavik Mehta]

noncomputable def zmultiples_equiv {G : Type*} [AddCommGroup G] (x : G) (hx : ¬ IsOfFinAddOrder x) :
    ℤ ≃+ AddSubgroup.zmultiples x where

This isn't hard to make, but I'm wondering if we have it in mathlib already?

[Jz Pan]

I think AddGroup is enough, and you can write ZMod (addOrderOf x) ≃+ AddSubgroup.zmultiples x in general.

Also it's best write a Group version then @[to_additive].

[Aaron Liu]

what's the group version? does it use Multiplicative (ZMod (orderOf x))?

[Bhavik Mehta]

Right, I specifically picked the additive version because the multiplicative version needs Multiplicative, and I want to avoid this indirection. And similarly the reason I used ℤ rather than ZMod was to avoid composing with another equality in my application. But if you're aware of a version in mathlib which uses ZMod, that'd be helpful too.

[Yaël Dillies]

There are things around docs#AddAction.zmultiplesQuotientStabilizerEquiv. None of them is exactly what you want, though

[Jz Pan]

I'm afraid that there are already results in mathlib mentioning Multiplicative, ZMod and orderOf. For example

• zmodCyclicMulEquiv :clipboard: Mathlib.GroupTheory.SpecificGroups.Cyclic
  {G : Type u_2} [Group G] (h : IsCyclic G) : Multiplicative (ZMod (Nat.card G)) ≃* G

[Bhavik Mehta]

Jz Pan said:

I'm afraid that there are already results in mathlib mentioning Multiplicative, ZMod and orderOf. For example

• zmodCyclicMulEquiv :clipboard: Mathlib.GroupTheory.SpecificGroups.Cyclic
  {G : Type u_2} [Group G] (h : IsCyclic G) : Multiplicative (ZMod (Nat.card G)) ≃* G

Indeed, and you'll notice that this is a great example of my point: it doesn't have to_additive applied to it!

[Jz Pan]

So the additive version is written manually?

[Bhavik Mehta]

Yes, exactly

[Bhavik Mehta]

In fact, the additive version is written manually and the multiplicative version is derived from it: https://github.com/leanprover-community/mathlib4/blob/850f9cbdcd1e365c8eca868785fb7874b6059d85/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean#L740

[Edward van de Meent]

sometimes i wish to_additive were able to add/remove Additive/Multiplicative respectively

[Edward van de Meent]

i wonder if that's something feasible