mathlib3

223f1496 - chore(algebra/star/self_adjoint): extract a lemma from `has_scalar` (#12121)