Some mathlib contributions Subject Algebra algebra of endomorphisms are central pi-types of star-ordered rings intrinsic star on linear maps star projections star structure on tensor products star-algebra automorphism given by unitary conjugation Analysis adjoint (co)algebra space inner product on opposite spaces inner product on tensor products partial order on matrices characterization of continuous (star-)algebra equivalences between continuous endormorphisms square roots on RCLike Linear Algebra characterization of algebra equivalences between endomorphisms Ring Theory coalgebra on opposite spaces