mathlib

0a31295e - feat(algebra/star/self_adjoint): add `star_mul_self`, `mul_star_self` and `star_hom_apply` (#16193)

feat(algebra/star/self_adjoint): add `star_mul_self`, `mul_star_self` and `star_hom_apply` (#16193) add some basic missing lemmas in the `is_self_adjoint` namespace: that `star x * x`, `x * (star x)` are selfadjoint, and members of a `star_hom_class` preserve self-adjoint elements.