Commit 2021-10-13 07:56 2c8abe52
View on Github →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.