mathlib

53f074ca - fix(data/complex/basic): better formulas for nsmul and gsmul on complex to fix a diamond (#8928)

fix(data/complex/basic): better formulas for nsmul and gsmul on complex to fix a diamond (#8928) As diagnosed by @eric-wieser in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/diamond.20in.20data.2Ecomplex.2Emodule/near/250318167 After the PR, ```lean example : (sub_neg_monoid.has_scalar_int : has_scalar ℤ ℂ) = (complex.has_scalar : has_scalar ℤ ℂ) := rfl ``` works fine, while it fails on current master.