mathlib

6fe90f28 - feat(algebra/jordan/special): The symmetrization of an associative ring is a commutative Jordan multiplication (#11401)

feat(algebra/jordan/special): The symmetrization of an associative ring is a commutative Jordan multiplication (#11401) 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). ``` When the original multiplication is associative, the symmetrised algebra is a commutative Jordan algebra. A commutative Jordan algebra which can be constructed in this way from an associative multiplication is said to be a special Jordan algebra. This PR shows more generally that for a ring where the scalar `2` is invertible, the symmetrised multiplication is a commutative Jordan multiplication. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>