mathlib3

1afdaf96 - feat(linear_algebra/trace): more general versions of `trace_mul_comm` and `trace_conj` (#13874)