## Stream: maths

### Topic: Scalar multiplication not defined for functions

#### Abhimanyu Pallavi Sudhir (Nov 22 2018 at 21:55):

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 (Nov 22 2018 at 21:56):

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 (Nov 22 2018 at 21:58):

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

#### Kevin Buzzard (Nov 22 2018 at 22:00):

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 (Nov 22 2018 at 22:01):

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

Last updated: May 12 2021 at 06:14 UTC