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 Data integer Fibonacci Cassini and Catalan identities for Fibonacci numbers Linear Algebra characterization of algebra equivalences between endomorphisms Ring Theory coalgebra on opposite spaces all PRs