add_group to group and back

Stream: new members

[Fedor Pavutnitskiy]

I'm trying to prove that zmod n is a group. Using apply_instance I can show that it is an add_group. Is there a way to move back and forth between these two ?

[Johan Commelin]

@Fedor Pavutnitskiy multiplicative (zmod n) is automatically a group.

[Johan Commelin]

zmod n has a multiplication and addition, making it into a ring. But the multiplicative structure is not a group, unless n = 1.

[Johan Commelin]

So making an instance of group (zmod n) will make Lean mightily confused, because it will not know which multiplication you are referring to when you write x * y.

[Fedor Pavutnitskiy]

Johan Commelin said:

Fedor Pavutnitskiy multiplicative (zmod n) is automatically a group.

exactly what I need, thanks a lot @Johan Commelin