mathlib3

feat(algebra/jordan/triple): Introduce Jordan triples

#11553

Open