Scalar multiplication by reals is continuous

Stream: Is there code for X?

[Bhavik Mehta]

import topology.instances.real_vector_space

open_locale classical

instance {n : ℕ} : has_continuous_smul ℝ (fin n → ℝ) := infer_instance

What do I need to import for this to be automatic?

[Eric Wieser]

What docs docs#has_continuous_smul have to say about the instances that exist?

[Bhavik Mehta]

Ah - importing normed spaces works. Thanks

[Eric Wieser]

I feel like there's still an instance missing here though; something like this should be true, right?

instance {R : Type*} {ι : Type*} {f : ι → Type*}
  [Π i, has_scalar R (f i)] [∀ i, topological_space(f i)] [∀ i, has_continuous_smul R (f i)] :
  has_continuous_smul R (Π i, f i) := sorry

that is, the pi version of docs#prod.has_continuous_smul