Tactic

Supporting modules for Euclidean Jordan algebras: power associativity, the spectral theorem, the trace form, Koecher/Alfsen-Shultz, and the frame Peirce decomposition.