diamond in data.complex.module

Stream: general

[Heather Macbeth]

I just hit what seems to be two competing instances of the ℤ-action on ℂ; wanted to report it in case it's not known.

import data.complex.module

-- this fails
example :
  (sub_neg_monoid.has_scalar_int : has_scalar ℤ ℂ) = (complex.has_scalar : has_scalar ℤ ℂ) :=
rfl

[Eric Wieser]

For reference: docs#complex.has_scalar, docs#complex.comm_ring.

[Eric Wieser]

The latter has the wrong definition of nsmul and gsmul

[Eric Wieser]

They need to both be defined as λ r x, ⟨r • x.re - 0 * x.im, r • x.im + 0 * x.re⟩

[Eric Wieser]

(to match the has_scalar, which in turn matches (↑r) * x when r : ℝ)