MIL exercise

Stream: lean4

[Katherine Wei]

nstance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
  smul := zsmul₁
  zero_smul := by exact fun m ↦ rfl
  one_smul := sorry
  mul_smul := sorry
  add_smul := sorry
  smul_add := sorry

I am having problem in these following code. can anyone help me finished the sorry part?

[Ted Hwa]

You can find solutions to all the exercises at https://github.com/leanprover-community/mathematics_in_lean/tree/master/MIL

Within each chapter subdirectory, there is another subdirectory called "solutions". You can consult that whenever you get stuck.