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 <85fbb02ca4514343a46329a92ab18d1dede56561@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib