Documentation

LeanPool.EuclideanJordan.EuclideanJordan

Imports

Init
LeanPool.EuclideanJordan.EuclideanJordan.Block
LeanPool.EuclideanJordan.EuclideanJordan.Bridge
LeanPool.EuclideanJordan.EuclideanJordan.Class
LeanPool.EuclideanJordan.EuclideanJordan.Connection
LeanPool.EuclideanJordan.EuclideanJordan.FormallyReal
LeanPool.EuclideanJordan.EuclideanJordan.Frame
LeanPool.EuclideanJordan.EuclideanJordan.FrameExists
LeanPool.EuclideanJordan.EuclideanJordan.FramePeirce
LeanPool.EuclideanJordan.EuclideanJordan.FramePeirceMul
LeanPool.EuclideanJordan.EuclideanJordan.HermitianBilin
LeanPool.EuclideanJordan.EuclideanJordan.HermitianCarrier
LeanPool.EuclideanJordan.EuclideanJordan.Order
LeanPool.EuclideanJordan.EuclideanJordan.OrderAuto
LeanPool.EuclideanJordan.EuclideanJordan.OrderUnitSpace
LeanPool.EuclideanJordan.EuclideanJordan.Orthogonal
LeanPool.EuclideanJordan.EuclideanJordan.Pattern
LeanPool.EuclideanJordan.EuclideanJordan.Peirce
LeanPool.EuclideanJordan.EuclideanJordan.PeirceMul
LeanPool.EuclideanJordan.EuclideanJordan.PeirceSubalgebra
LeanPool.EuclideanJordan.EuclideanJordan.Power
LeanPool.EuclideanJordan.EuclideanJordan.PowerAssoc
LeanPool.EuclideanJordan.EuclideanJordan.Rank
LeanPool.EuclideanJordan.EuclideanJordan.Spectral
LeanPool.EuclideanJordan.EuclideanJordan.Subalgebra
LeanPool.EuclideanJordan.EuclideanJordan.TraceForm
LeanPool.EuclideanJordan.EuclideanJordan.Witness
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.ContinuousLinearMap
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.IsMaximalSelfAdjoint
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Isometry
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.LinearEquiv
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Matrix
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Misc
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Basic
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.CFC
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Inner
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Jordan
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.NonSingular
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Order
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Proj
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Reindex
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Trace
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Tactic.Commutes
LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Tactic.Commutes.Attribute

Imported by

Euclidean Jordan algebras in Lean 4 #

Root import for the library. See README.md for the headline results.