Commit 2021-10-08 10:04 179a4952

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.