Scalar tower/restrict scalars for is_R_or_C

Stream: maths

[Moritz Doll]

If I have [is_R_or_C k] [module k E] what is the correct way to get a compatible instance of [module ℝ E]? explicitly asking for that and [is_scalar_tower ℝ k E] seems a bit stupid because the action is already determined, but using a similar definition as for the complex numbers (using normed_space.restrict_scalars) fails because of infinite recursion in type-class resolution

[Frédéric Dupuis]

[is_scalar_tower ℝ k E] is the way to go. From what I recall this instance you have there is bad because it loops when k is ℝ (I tried it at some point).

[Moritz Doll]

ok, thanks