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 inner product of opposite spaces inner product of tensor products partial order on matrices characterization of continuous (star-)algebra equivalences between continuous endormorphisms Linear Algebra characterization of algebra equivalences between endomorphisms Ring Theory coalgebra of opposite space