mathlib

b0805a5e - feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372)

feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372) Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com> Co-authored-by: Oliver Nash <github@olivernash.org>