Heterogeneous multiplication

Stream: general

[Eric Wieser]

We currently use has_scalar which lets us spell things like r • ![x, y] = ![r • x, r • y]. But what about if I want something like (X : polynomial R) • ![x, y] = ![polynomial.X * C x, polynomial.X * C y]? Do we want instances for this type of thing in lean4 when we have HMul? Does it still make sense to talk about these as "actions" in the same way?

[Eric Wieser]

I guess we would have to be careful of ambiguity like ![x, y] • ![a, b], which could mean ![![x•a, x•b], ![y•a, y•b]] or ![![x•a, y•a], ![x•b, y•b]], neither of which are what docs#pi.has_scalar' actually does today

[Reid Barton]

There is the tensor product which encompasses these two examples. Probably other random bilinear maps should not be a type class.