Commit 2021-03-23 19:49 9cda1ff6

fix(data/complex/module): kill a non-defeq diamond (#6760) restrict_scalars.semimodule ℝ ℂ ℂ = complex.semimodule is currently not definitionally true. The PR tweaks the smul definition to make sure that this becomes true. This solves a diamond that appears naturally in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60inner_product_space.20.E2.84.9D.20%28euclidean_space.20.F0.9D.95.9C.20n%29.60.3F/near/230780186