feat(algebra/star/algebra): generalize to modules (#9484)
This means there is now a `star_module ℂ (ι → ℂ)` instance available.
This adds `star_add_monoid`, and renames `star_algebra` to `star_module` with significantly relaxed typeclass arguments.
This also uses `export` to cut away some unnecessary definitions, and adds the missing `pi.star_def` to match `pi.add_def` etc.
