matrix.dot_product is a linear map

Stream: Is there code for X?

[Eric Wieser]

Do we have docs#matrix.dot_product as a bundled linear map in one / both arguments?

[Johan Commelin]

For the liquid project, it would be great to have something that takes a matrix of integers, and spits out an add_monoid_hom A^m ->+ A^n (where A is an add_comm_group)

[Johan Commelin]

This can be generalised to arbitrary semirings and semimodules, I guess.

[Eric Wieser]

Isn't what you're asking for docs#matrix.to_lin'?

[Johan Commelin]

Yup, except that one is linear, not just additive.