Commit 2022-03-03 23:56 40524f19
View on Github →feat(algebra/star/self_adjoint): define normal elements of a star monoid (#11991)
In this PR, we define the normal elements of a star monoid, i.e. those elements x
that commute with star x. This is defined as the prop type class is_star_normal.
This was formalized as part of the semilinear maps paper.