Scalar multiplication on functions

Stream: Is there code for X?

[Bolton Bailey]

Do we have an instance for has_scalar F (D → F) where F is a field?

[Yaël Dillies]

docs#pi.has_scalar + docs#has_mul.to_has_scalar

[Bolton Bailey]

Why is this giving me a failed to synthesize type class error?

import data.polynomial.basic
import group_theory.group_action.pi
import group_theory.group_action.defs

variables {D F : Type*} [fintype D] [fintype F] [field F]

def eval_parameterized_curve {D} (l : ℕ) (z : F)
  (u : D -> F) : D -> F := z • u

[Bolton Bailey]

Oh weird, it was the {D}

[Yaël Dillies]

Yes, because you had D : Sort*, but pi.has_scalar only works for D : Type*. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Sort-indexed.20pi.20type

[Eric Wieser]

Yaël Dillies' link is relevant but the claim is misrepresented; pi.has_scalar isn't to blame, has_scalar is:

example {D : Sort*} {F : Type*} : has_scalar F (D → F) := sorry  -- fails

[Yaël Dillies]

I mean yeah, the long story is the thread I linked to :stuck_out_tongue: