Left injection function for the inner product From a vector space (and also group and module) perspective the product is the same as the sum of two vector spaces. inl and inr provide the corresponding injection functions.

Right injection function for the inner product