Commit 2021-12-31 19:13 fbbbdfa0

feat(algebra/star/self_adjoint): define the self-adjoint elements of a star additive group (#11135) Given a type R with [add_group R] [star_add_monoid R], we define self_adjoint R as the additive subgroup of self-adjoint elements, i.e. those such that star x = x. To avoid confusion, we move is_self_adjoint (which defines this to mean ⟪T x, y⟫ = ⟪x, T y⟫ in an inner product space) to the inner_product_space namespace.