Zulip Chat Archive

Stream: maths

Topic: Scalar multiplication not defined for functions


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 22 2018 at 21:58):

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

view this post on Zulip 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 α}

view this post on Zulip 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