mathlib

f63b8f12 - feat(algebra/star/basic): add some helper lemmas about star (#9651)

feat(algebra/star/basic): add some helper lemmas about star (#9651) This adds the new lemmas: * `star_pow` * `star_nsmul` * `star_gsmul` * `star_prod` * `star_div` * `star_div'` * `star_inv` * `star_inv'` * `star_mul'` and generalizes the typeclass assumptions from `star_ring` to `star_add_monoid` on: * `star_neg` * `star_sub` * `star_sum`