Scalar multiplication not defined for functions

Stream: maths

[Abhimanyu Pallavi Sudhir]

It seems that smul over ℝ isn't defined for functions from ℝ to ℝ -- or at least, I can't get it to work.

[Abhimanyu Pallavi Sudhir]

It seems to me that functions are a rather natural type to use scalar multiplication on -- or am I missing some trick?

[Abhimanyu Pallavi Sudhir]

(also, should there be a coercion from α to β → α -- i.e. to constant functions?)

[Kevin Buzzard]

Chris Hughes suggested that importing pi_instances might fix this -- but it didn't seem to.

import data.real.basic
import algebra.module
import algebra.pi_instances

example : module ℝ ℝ := by apply_instance
example : has_scalar ℝ (ℝ → ℝ) := by apply_instance -- fails

pi_instances contains the line

instance module       (α) {r : ring α}           [∀ i, add_comm_group $ f i]  [∀ i, module α $ f i]       : module α (Π i : I, f i)       := {..pi.semimodule α}

[Kevin Buzzard]

import data.real.basic
import algebra.module
import algebra.pi_instances

example : module ℚ ℚ := by apply_instance
example : has_scalar ℚ (ℚ → ℚ) := by apply_instance -- fails

That fails too so it's not some decidable equality issue