Documentation

LeanPool.EuclideanJordan

Euclidean Jordan algebras and the frame Peirce decomposition #

Source: url:https://github.com/ehrlich-b/euclidean-jordan Authors: Bryan Ehrlich Status: verified Main declarations: EuclideanJordan.frameBlock_isInternal Tags: nonassociative-algebra MSC: 17C20, 17C27, 17C37, 17C65, 17A15, 46L70