mathlib3
chore(analysis/normed_space/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
urkud urkud added awaiting-review
eric-wieser
eric-wieser commented on 2021-03-22
sgouezel sgouezel removed awaiting-review
sgouezel sgouezel added awaiting-author
github-actions github-actions added merge-conflict
eric-wieser eric-wieser force pushed from 7a7eec24 to d081e57e 3 years ago
eric-wieser chore(analysis/inner_product_space/pi_L2): euclidean space is a real …
e4d0b0e9
eric-wieser fix errors
0c0dadf8
eric-wieser eric-wieser force pushed from d081e57e to 0c0dadf8 3 years ago
eric-wieser
eric-wieser commented on 2023-03-14
eric-wieser
eric-wieser eric-wieser removed merge-conflict
urkud
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone