Commit 2022-01-15 14:19 ce62dbc3

feat(algebra/star/self_adjoint): module instance on self-adjoint elements of a star algebra (#11322) We put a module instance on self_adjoint A, where A is a [star_module R A] and R has a trivial star operation. A new typeclass [has_trivial_star R] is created for this purpose with an instance on ℝ. This allows us to express the fact that e.g. the space of complex Hermitian matrices is a real vector space.