Commit 2022-02-25 03:05 605ea9f3
View on Github →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