mathlib

65eef746 - 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' ```