Skip to content

Import Euclidean Jordan algebras and frame Peirce decomposition #477

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 22 commits into
base: main
Choose a base branch
from
Open

Import Euclidean Jordan algebras and frame Peirce decomposition #477

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
b324e65
Import complete euclidean-jordan proof development
Vilin97 Sep 21, 2026
c9d8232
Advance euclidean-jordan port to Lean 4.34
Vilin97 Sep 21, 2026
6cda2b8
Port the complete Euclidean Jordan development to Lean 4.34
Vilin97 Sep 21, 2026
c1cf1d9
Complete Euclidean Jordan port and document matrix and frame APIs
Vilin97 Sep 21, 2026
45af422
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 22, 2026
361a9ef
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 23, 2026
3f7ae7f
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 23, 2026
7484930
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 24, 2026
9d1e4de
Expose Euclidean Jordan algebra modules
Vilin97 Sep 25, 2026
1b61979
Sync current main for module checks
Vilin97 Sep 25, 2026
f2c77c6
Remove duplicate Euclidean Jordan license headers
Vilin97 Sep 25, 2026
db56e96
Merge commit 'da8a453e14ddf6218c1d3d10ff27ca7765dfef77' into HEAD
Vilin97 Sep 25, 2026
305646b
Merge commit '0e9b057b62cc4eaa1b4a42cf23766cf7b9bd3537' into HEAD
Vilin97 Sep 25, 2026
f76f602
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
26619de
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
7bbdd43
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
3b4ea6d
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
f7808c3
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
b8ffc42
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
e40717d
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
e77d34d
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
c19522d
Merge remote-tracking branch 'origin/main' into pr-477
github-actions[bot] Sep 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 53 additions & 0 deletions LeanPool.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2476,6 +2476,59 @@ public import LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N2
public import LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3JoinN3N2
public import LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3N2
public import LeanPool.ErdosTuzaValtr.Main.Main
public import LeanPool.EuclideanJordan
public import LeanPool.EuclideanJordan.EuclideanJordan
public import LeanPool.EuclideanJordan.EuclideanJordan.Block
public import LeanPool.EuclideanJordan.EuclideanJordan.Bridge
public import LeanPool.EuclideanJordan.EuclideanJordan.Class
public import LeanPool.EuclideanJordan.EuclideanJordan.Connection
public import LeanPool.EuclideanJordan.EuclideanJordan.FormallyReal
public import LeanPool.EuclideanJordan.EuclideanJordan.Frame
public import LeanPool.EuclideanJordan.EuclideanJordan.FrameExists
public import LeanPool.EuclideanJordan.EuclideanJordan.FramePeirce
public import LeanPool.EuclideanJordan.EuclideanJordan.FramePeirceMul
public import LeanPool.EuclideanJordan.EuclideanJordan.HermitianBilin
public import LeanPool.EuclideanJordan.EuclideanJordan.HermitianCarrier
public import LeanPool.EuclideanJordan.EuclideanJordan.Order
public import LeanPool.EuclideanJordan.EuclideanJordan.OrderAuto
public import LeanPool.EuclideanJordan.EuclideanJordan.OrderUnitSpace
public import LeanPool.EuclideanJordan.EuclideanJordan.Orthogonal
public import LeanPool.EuclideanJordan.EuclideanJordan.Pattern
public import LeanPool.EuclideanJordan.EuclideanJordan.Peirce
public import LeanPool.EuclideanJordan.EuclideanJordan.PeirceMul
public import LeanPool.EuclideanJordan.EuclideanJordan.PeirceSubalgebra
public import LeanPool.EuclideanJordan.EuclideanJordan.Power
public import LeanPool.EuclideanJordan.EuclideanJordan.PowerAssoc
public import LeanPool.EuclideanJordan.EuclideanJordan.Rank
public import LeanPool.EuclideanJordan.EuclideanJordan.Spectral
public import LeanPool.EuclideanJordan.EuclideanJordan.Subalgebra
public import LeanPool.EuclideanJordan.EuclideanJordan.TraceForm
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.ContinuousLinearMap
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Basic
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.CFC
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Inner
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Jordan
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.NonSingular
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Order
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Proj
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Reindex
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.HermitianMat.Trace
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.IsMaximalSelfAdjoint
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Isometry
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.LinearEquiv
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Matrix
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Misc
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Tactic
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Tactic.Commutes
public import LeanPool.EuclideanJordan.EuclideanJordan.Vendor.Tactic.Commutes.Attribute
public import LeanPool.EuclideanJordan.EuclideanJordan.Witness
public import LeanPool.EuclideanJordan.FramePeirceSolution
public import LeanPool.EuclideanJordan.KoecherSolution
public import LeanPool.EuclideanJordan.SpectralSolution
public import LeanPool.EuclideanJordan.StructureSolution
public import LeanPool.EuclideanJordan.TraceFormSolution
public import LeanPool.EvenGraphCycles
public import LeanPool.EventStructures
public import LeanPool.EventStructures.Basic
Expand Down
74 changes: 74 additions & 0 deletions LeanPool/EuclideanJordan.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
/-
Copyright (c) 2026 Bryan Ehrlich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bryan Ehrlich
-/

module

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


/-!
# 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
-/

@[expose] public section
59 changes: 59 additions & 0 deletions LeanPool/EuclideanJordan/EuclideanJordan.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
/-
Copyright (c) 2026 Bryan Ehrlich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bryan Ehrlich
-/
module

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


/-!
# Euclidean Jordan algebras in Lean 4

Root import for the library. See `README.md` for the headline results.
-/

@[expose] public section
Loading
Loading