feat(linear_algebra/trace): trace of prod_map (#13872)
In this PR I prove that the trace is additive under `prod_map`, i.e. that `trace (prod_map f g) = trace f + trace g`.
Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>
