mathlib

40524f19 - feat(algebra/star/self_adjoint): define normal elements of a star monoid (#11991)

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. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>