feat(linear_algebra/orientation): inherit an action by `units R` on `module.ray R M` (#10738)
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.






leanprover-community/mathlib,leanprover-community/mathlib