Skip to content

feat: complexification of inner product spaces #88

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
themathqueen wants to merge 32 commits into
base: master
Choose a base branch
from
Open

feat: complexification of inner product spaces #88

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
46bb50e
complexification of inner product spaces
themathqueen Aug 5, 2026
6006999
mk_all
themathqueen Aug 5, 2026
081bf62
update
themathqueen Aug 5, 2026
bc29220
move file and add more API
themathqueen Aug 5, 2026
8874c3b
lake mk_all
themathqueen Aug 5, 2026
6c27458
fix
themathqueen Aug 5, 2026
82a6665
some more API
themathqueen Aug 5, 2026
4efbf8d
fix
themathqueen Aug 5, 2026
cd45799
fix again
themathqueen Aug 5, 2026
959ae02
cleanup
themathqueen Aug 5, 2026
3c756c3
more stuff
themathqueen Aug 7, 2026
261e96a
golf
themathqueen Aug 7, 2026
2890082
just some docs
themathqueen Aug 7, 2026
14b1537
just some refactors
themathqueen Aug 7, 2026
34fb23e
remove the other version, no need
themathqueen Aug 7, 2026
385e1ed
toMatrix
themathqueen Aug 7, 2026
e971039
remove trace import
themathqueen Aug 7, 2026
d3a01bc
cfc and split file
themathqueen Aug 8, 2026
3f94f41
lake mk_all
themathqueen Aug 8, 2026
b3648d3
random cleanup
themathqueen Aug 8, 2026
6f027d4
more
themathqueen Aug 8, 2026
749866d
references
themathqueen Aug 8, 2026
62b3f37
cleanup
themathqueen Aug 8, 2026
c1df558
cfc for rclike
themathqueen Aug 9, 2026
c59568e
fix
themathqueen Aug 9, 2026
66974bc
bit more cleanup
themathqueen Aug 9, 2026
ba0e37a
more cleanup
themathqueen Aug 9, 2026
5a633b3
more api
themathqueen Aug 9, 2026
c62da4c
typos
themathqueen Aug 9, 2026
58f80dc
more cleanup
themathqueen Aug 9, 2026
03f65e2
final cleanup?
themathqueen Aug 9, 2026
4a3cc6d
tiny cleanup
themathqueen Aug 11, 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
3 changes: 3 additions & 0 deletions LeanOA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,9 @@ public import LeanOA.Mathlib.Analysis.CStarAlgebra.Module.Defs
public import LeanOA.Mathlib.Analysis.CStarAlgebra.MulNonneg
public import LeanOA.Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
public import LeanOA.Mathlib.Analysis.Complex.Basic
public import LeanOA.Mathlib.Analysis.InnerProductSpace.Complexification.Basic
public import LeanOA.Mathlib.Analysis.InnerProductSpace.Complexification.Transfers
public import LeanOA.Mathlib.Analysis.InnerProductSpace.Orthogonal
public import LeanOA.Mathlib.Analysis.LocallyConvex.Bipolar
public import LeanOA.Mathlib.Analysis.LocallyConvex.Bounded
public import LeanOA.Mathlib.Analysis.LocallyConvex.IsCompatibleDual
Expand Down
Loading
Loading