mathlib3
e4d0b0e9 - chore(analysis/inner_product_space/pi_L2): euclidean space is a real inner product space

Commit
2 years ago
chore(analysis/inner_product_space/pi_L2): euclidean space is a real inner product space
Author
Committer
Parents
Loading