feat(analysis/von_neumann_algebra/basic): one result #18290
themathqueen
wants to merge
44 commits into
master
from
vna
feat(analysis/inner_product_space/finite_dimensional): created new fi…
455c5aa1
Fix style
4cb7241c
fix
3a4a1789
fix after review
3c1f3c1f
3 new results
337a7333
final result for now
7288bfaf
fix
1e23e67d
Update fix
6e955ff5
fixes after review
c65fa8a1
fixes after review
8577cc5e
Add von Neumann file here
18ba6fd7
delete comment
1d54562b
fixed names and other stuff and added more lemmas
f20143f3
fix
a1309907
added a bit more
357d1513
fix
abc7b99a
linear_map.sqrt
dd129bee
fix and one lemma
28eee7d1
fix
bc5c1572
move lemmas on dual to other pr
b98f2e14
fix
27054bf0
tiny fix
5a236bc0
fix
a9892e18
moved stuff
833b4b9b
fix after review
c8413dcf
fix
b6484a29
Express `orthogonal_projection` as `linear_proj_of_is_compl`
a2d7a240
fix after review
4c29708c
fix
239b4674
fix after review
5b6547e9
Merge branch 'master' of https://github.com/leanprover-community/math…
465b309a
Merge branch 'AD_ortho_proj_is_linear_proj' of https://github.com/lea…
9bdaf700
merge branches
a0dc536a
typo
b6765404
fix
2f5c69d0
fix after review
d984f884
feat(linear_algebra/invariant_submodule): invariant submodules
a7cd215b
moved files to new PR
a609fed1
Merge branch 'invariant_submodule' of https://github.com/leanprover-c…
fbdbd949
move file to new pr
537fc76f
feat(analysis/von_neumann_algebra): one result
47ab0ab6
added lemmas for clm
c5d3db0b
Merge branch 'finite_dimensional_inner_product_spaces' of https://git…
1a3d4d6a
moved result to /basic
d059346d
themathqueen
changed the title 
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review
blocked-by-other-PR
t-analysis
not-too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub