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

feat(analysis/inner_product_space/finite_dimensional): created new file for finite dimensional inner product space

themathqueen committed 3 years ago

Fix style

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

fix after review

themathqueen committed 3 years ago

3 new results

themathqueen committed 3 years ago

final result for now

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

Update fix

themathqueen committed 3 years ago

fixes after review

themathqueen committed 3 years ago

fixes after review

themathqueen committed 3 years ago

Add von Neumann file here

themathqueen committed 3 years ago

delete comment

themathqueen committed 3 years ago

fixed names and other stuff and added more lemmas

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

added a bit more

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

linear_map.sqrt

themathqueen committed 3 years ago

fix and one lemma

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

move lemmas on dual to other pr

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

tiny fix

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

moved stuff

themathqueen committed 3 years ago

fix after review

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

Express `orthogonal_projection` as `linear_proj_of_is_compl`

ADedecker committed 3 years ago

fix after review

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

fix after review

themathqueen committed 3 years ago

Merge branch 'master' of https://github.com/leanprover-community/mathlib into finite_dimensional_inner_product_spaces

themathqueen committed 3 years ago

Merge branch 'AD_ortho_proj_is_linear_proj' of https://github.com/leanprover-community/mathlib into finite_dimensional_inner_product_spaces

themathqueen committed 3 years ago

merge branches

themathqueen committed 3 years ago

typo

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

fix after review

themathqueen committed 3 years ago

feat(linear_algebra/invariant_submodule): invariant submodules

themathqueen committed 3 years ago

moved files to new PR

themathqueen committed 3 years ago

Merge branch 'invariant_submodule' of https://github.com/leanprover-community/mathlib into finite_dimensional_inner_product_spaces

themathqueen committed 3 years ago

move file to new pr

themathqueen committed 3 years ago

added lemmas for clm

themathqueen committed 3 years ago

move non-finitedimensional stuff to other file

themathqueen committed 3 years ago

moved stuff

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

fix

themathqueen committed 3 years ago

move stuff

themathqueen committed 3 years ago

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

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

Open