inner_product): euclidean space is a real inner product space
#6799

Open

chore(analysis/normed_space/inner_product): euclidean space is a real inner product space #6799

urkud wants to merge 2 commits into master from eu-space-instance

urkud added awaiting-review

eric-wieser commented on 2021-03-22

sgouezel removed awaiting-review

sgouezel added awaiting-author

github-actions added merge-conflict

eric-wieser force pushed from 7a7eec24 to d081e57e 3 years ago

chore(analysis/inner_product_space/pi_L2): euclidean space is a real …

e4d0b0e9

fix errors

0c0dadf8

eric-wieser force pushed from d081e57e to 0c0dadf8 3 years ago

eric-wieser commented on 2023-03-14

eric-wieser removed merge-conflict

kim-em added too-late

Reviewers

eric-wieser

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone