mathlib3

b68f3403 - feat(ring_theory/trace): trace of product rings (#18656)

feat(ring_theory/trace): trace of product rings (#18656) Probably not a very useful result, but thought I'd add it to get some intuition for `trace`. I didn't bother with `pi` because we don't have the analogous `linear_map.trace` statements either.