mathlib

88863864 - feat(star/basic): add a `star_monoid (units R)` instance (#9681)

feat(star/basic): add a `star_monoid (units R)` instance (#9681) This also moves all the `opposite R` instances to be adjacent, and add some missing `star_module` definitions.