mathlib

605ea9f3 - feat(algebra/symmetrized): Define the symmetrization of a ring (#11399)

feat(algebra/symmetrized): Define the symmetrization of a ring (#11399) A commutative multiplication on a real or complex space can be constructed from any multiplication by "symmetrisation" i.e ``` a∘b = 1/2(ab+ba). ``` The approach taken here is inspired by `algebra.opposites`. Previously submitted as part of #11073. Will be used in https://github.com/leanprover-community/mathlib/pull/11401 Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>