unique Z-module structure on any AddCommGroup

Stream: Is there code for X?

[Kenny Lau]

instance uniqueIntModule (R : Type u) [AddCommGroup R] : Unique (Module ℤ R) :=
  ⟨⟨inferInstance⟩, fun m ↦ Module.ext <| funext₂ <| fun n x ↦ Int.induction_on n
    ((m.zero_smul _).trans (zero_smul ..).symm)
    (fun n ih ↦ (m.add_smul ..).trans <| (congr_arg₂ (· + ·) ih (m.one_smul _)).trans <|
      by rw [SMul.smul_eq_hSMul, add_one_zsmul])
    (fun n ih ↦ (m.add_smul ..).trans <| (congr_arg₂ (· + ·) ih (neg_one_smul _ _)).trans <|
      by rw [SMul.smul_eq_hSMul, sub_one_zsmul])⟩

[Kenny Lau]

oh wait, it is AddCommGroup.uniqueIntModule lol with the same name

[Kenny Lau]

it's not an instance because:

/-- All `ℤ`-module structures are equal. Not an instance since in mathlib all `AddCommGroup`
should normally have exactly one `ℤ`-module structure by design. -/

[Kenny Lau]

hmm according to the logic of the doc, maybe I'm having an XY-problem!

[Kenny Lau]

moved to #Is there code for X? > failed to synthesize `CommRing (R ⊗[ℤ] Localization M)`