mathlib

2c8abe52 - feat(algebra/star): `star_gpow` and `star_fpow` (#9661)

feat(algebra/star): `star_gpow` and `star_fpow` (#9661) One unrelated proof changes as the import additions pulls in a simp lemma that was previously missing, making the call to `ring` no longer necessary.