Prove known function is group isomorphism

Stream: Is there code for X?

[Ben]

Given I have def phi (n: ℤ) := -n how do I write the lean proof to show it is a additive group isomorphism? I know how to show types have group properties with @[instance] def ℤ.group : group ℤ := {...}but am struggling to replicate this using the iso structure thingy.

[Yaël Dillies]

import algebra.hom.equiv

variables {α : Type*} [add_comm_group α]

def add_equiv.neg_iso : α ≃+ α :=
{ to_fun := λ a, -a ,
  inv_fun := λ a, -a,
  left_inv := sorry,
  right_inv := sorry,
  map_add' := sorry }

[Kevin Buzzard]

You maybe shouldn't define the bare phi at all (after all, we have it already, it's called has_neg.neg with notation -) but should instead let phi be add_equiv.neg_iso and enjoy the fact that it will coerce to a function automatically.