## Stream: new members

### Topic: type class inference for has_scalar

#### Jan-David Salchow (Nov 05 2018 at 15:07):

The type class mechanism doesn't seem be able to figure out that functions to a normed space can be multiplied by scalars. Does anybody know why?

import analysis.normed_space algebra.pi_instances

-- works
example {α E : Type*} [vector_space ℝ E] (c : ℝ) (f : α → E) : ∀ x : α, (c • f) x  = c • (f x) := by simp

-- works
example {α E : Type*} [normed_space ℝ E] (c : ℝ) (f : α → E) :
∀ x : α, (@has_scalar.smul _ _ (@pi.has_scalar _ _ _ _) c f) x  =  c • (f x) :=
by simp

-- doesn't work
example {α E : Type*} [normed_space ℝ E] (c : ℝ) (f : α → E) : ∀ x : α, (c • f) x  = c • (f x) := by simp


#### Mario Carneiro (Nov 05 2018 at 15:10):

what is c • f?

#### Mario Carneiro (Nov 05 2018 at 15:10):

oh I see it's the pi instance

Last updated: May 14 2021 at 12:18 UTC