mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

feat(algebra/jordan/special): Introduce special Jordan algebras

Open mans0954 opened this issue 4 years ago • 1 comments

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.

Previously included as part of #11073

  • [x] depends on: #11073
  • [x] depends on: #11399

Open in Gitpod

mans0954 avatar Jan 12 '22 20:01 mans0954

This PR/issue depends on:

  • ~~leanprover-community/mathlib#11073~~
  • ~~leanprover-community/mathlib#11399~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Jul 26 '22 06:07 mathlib-dependent-issues-bot

@eric-wieser Are you able to approve this now?

mans0954 avatar Aug 23 '22 21:08 mans0954

Is the PR title still accurate? I was expecting to see something like

class special_jordan_algebra (α : Type*) [something α] : Prop :=
(exists_sym : ∃ β [something_else β], α ≃+* sym β)

I can't recall what I originally had in mind now, so I've updated the title and opening comment to reflect how it's ended up.

mans0954 avatar Aug 30 '22 14:08 mans0954

@jcommelin Please would you be willing to review this PR? It's had quite a bit of review already, so hopefully is in a good shape.

mans0954 avatar Sep 23 '22 07:09 mans0954

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Sep 28 '22 06:09 bors[bot]