mathlib
edb7f923 - feat(algebra/jordan): Introduce Jordan rings (#11073)

Commit
3 years ago
feat(algebra/jordan): Introduce Jordan rings (#11073) Introduces linear Jordan rings; linearises the Jordan axiom; shows that every associative ring has a symmertised product with respect to which it is a commutative Jordan ring. Linearising the Jordan axiom is an important step towards showing that (commutative) Jordan algebras are power associative. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Author
Parents
Loading