finite_dimensional): some lemmas on finite dimensional inner product spaces
#18041

Open

feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces #18041

themathqueen wants to merge 48 commits into master from finite_dimensional_inner_product_spaces

feat(analysis/inner_product_space/finite_dimensional): created new fi…

455c5aa1

themathqueen added WIP

themathqueen added awaiting-review

themathqueen added t-analysis

themathqueen removed WIP

Fix style

4cb7241c

themathqueen requested a review from

urkud 3 years ago

themathqueen requested a review from

hrmacbeth 3 years ago

themathqueen requested a review from

RemyDegenne 3 years ago

themathqueen requested a review from

dupuisf 3 years ago

eric-wieser commented on 2023-01-02

ADedecker assigned

ADedecker 3 years ago

fix

3a4a1789

themathqueen requested a review from

eric-wieser 3 years ago

eric-wieser commented on 2023-01-03

fix after review

3c1f3c1f

themathqueen requested a review from

eric-wieser 3 years ago

3 new results

337a7333

themathqueen requested a review from

ADedecker 3 years ago

final result for now

7288bfaf

fix

1e23e67d

eric-wieser commented on 2023-01-04

Update fix

6e955ff5

eric-wieser commented on 2023-01-04

eric-wieser removed awaiting-review

eric-wieser added awaiting-author

fixes after review

c65fa8a1

themathqueen requested a review from

eric-wieser 3 years ago

themathqueen removed awaiting-author

themathqueen added awaiting-review

eric-wieser commented on 2023-01-06

fixes after review

8577cc5e

Add von Neumann file here

18ba6fd7

themathqueen changed the title ~~feat(analysis/inner_product_space/finite_dimensional): new file~~ feat(analysis/inner_product_space/finite_dimensional & analysis/von_neumann_algebra/finite_dimensional): new files 3 years ago

themathqueen requested a review from

eric-wieser 3 years ago

delete comment

1d54562b

dupuisf commented on 2023-01-15

fixed names and other stuff and added more lemmas

f20143f3

themathqueen requested a review from

dupuisf 3 years ago

eric-wieser commented on 2023-01-16

fix

a1309907

added a bit more

357d1513

eric-wieser commented on 2023-01-17

fix

abc7b99a

linear_map.sqrt

dd129bee

fix and one lemma

28eee7d1

eric-wieser commented on 2023-01-19

fix

bc5c1572

eric-wieser commented on 2023-01-19

move lemmas on dual to other pr

b98f2e14

sgouezel commented on 2023-01-19

sgouezel removed awaiting-review

sgouezel added awaiting-author

fix

27054bf0

themathqueen removed awaiting-author

themathqueen added awaiting-review

tiny fix

5a236bc0

fix

a9892e18

moved stuff

833b4b9b

ADedecker commented on 2023-01-19

ADedecker removed awaiting-review

ADedecker added awaiting-author

fix after review

c8413dcf

themathqueen requested a review from

ADedecker 3 years ago

themathqueen removed awaiting-author

themathqueen added awaiting-review

fix

b6484a29

Express `orthogonal_projection` as `linear_proj_of_is_compl`

a2d7a240

ADedecker removed awaiting-review

ADedecker added awaiting-author

fix after review

4c29708c

fix

239b4674

themathqueen removed awaiting-author

themathqueen added awaiting-review

ADedecker commented on 2023-01-22

ADedecker removed awaiting-review

ADedecker added awaiting-author

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

themathqueen removed awaiting-author

themathqueen added awaiting-review

themathqueen requested a review from

ADedecker 3 years ago

typo

b6765404

eric-wieser commented on 2023-01-23

fix

2f5c69d0

ADedecker commented on 2023-01-23

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

themathqueen added blocked-by-other-PR

ghost removed blocked-by-other-PR

themathqueen changed the title ~~feat(analysis/inner_product_space/finite_dimensional & analysis/von_neumann_algebra/finite_dimensional): new files~~ feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces 3 years ago

move file to new pr

537fc76f

added lemmas for clm

c5d3db0b

Vierkantor added blocked-by-other-PR

move non-finitedimensional stuff to other file

09ad49a7

moved stuff

8e7a82c7

fix

05308bc5

fix

213ec182

fix

0fb02b47

fix

cf2106cf

move stuff

3a150f90

eric-wieser added not-too-late

Reviewers

ADedecker

eric-wieser

sgouezel

dupuisf

urkud

hrmacbeth

RemyDegenne

Assignees

ADedecker

Labels

awaiting-review blocked-by-other-PR t-analysis not-too-late

Milestone

No milestone

mathlib3 feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces #18041 Open

feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces #18041

mathlib3
feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces
#18041

Open