Commit 2021-12-13 09:36 e60899c5

feat(linear_algebra/orientation): inherit an action by units R on module.ray R M (#10738) This action is just the action inherited on the elements of the module under the quotient. We provide it generally for any group G that satisfies the required properties, but are only really interested in G = units R. This PR also provides module.ray.map, for sending a ray through a linear equivalence. This generalization also provides us with mul_action (M ≃ₗ[R] M) (module.ray R M), which might also turn out to be useful.