fix(data/int/basic): ensure the additive group structure on integers is computable (#9803)
fix(data/int/basic): ensure the additive group structure on integers is computable (#9803)

This prevents the following failure:
```lean
import analysis.normed_space.basic
instance whoops : add_comm_group ℤ := by apply_instance
-- definition 'whoops' is noncomputable, it depends on 'int.normed_comm_ring'
```






leanprover-community/mathlib,leanprover-community/mathlib