Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes

added theorem sym_alg.inv_of_sym
added theorem sym_alg.mul_comm
added theorem sym_alg.mul_def
added def sym_alg.sym
added theorem sym_alg.sym_add
added theorem sym_alg.sym_bijective
added theorem sym_alg.sym_comp_unsym
added theorem sym_alg.sym_eq_one_iff
added theorem sym_alg.sym_inj
added theorem sym_alg.sym_injective
added theorem sym_alg.sym_inv
added theorem sym_alg.sym_mul_self
added theorem sym_alg.sym_mul_sym
added theorem sym_alg.sym_ne_one_iff
added theorem sym_alg.sym_neg
added theorem sym_alg.sym_one
added theorem sym_alg.sym_smul
added theorem sym_alg.sym_sub
added theorem sym_alg.sym_surjective
added theorem sym_alg.sym_unsym
added def sym_alg.unsym
added theorem sym_alg.unsym_add
added theorem sym_alg.unsym_comp_sym
added theorem sym_alg.unsym_inj
added theorem sym_alg.unsym_inv
added theorem sym_alg.unsym_mul
added theorem sym_alg.unsym_mul_self
added theorem sym_alg.unsym_neg
added theorem sym_alg.unsym_one
added theorem sym_alg.unsym_smul
added theorem sym_alg.unsym_sub
added theorem sym_alg.unsym_sym
added def sym_alg