Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(measure_theory/l2_space): L2 is an inner product space #6596
[Merged by Bors] - feat(measure_theory/l2_space): L2 is an inner product space #6596
Changes from 76 commits
b2e2b05
5fb9cd3
2be7013
42aae48
51d51bc
b6b5096
1eb530e
817c7dc
27d3b46
c2207dd
29315d0
57def92
b2f92ad
04fdee7
fc16998
20cef34
7c3b693
8bae6fe
731a80f
29bad52
7f983e5
43a04d4
e608a7c
dac8f54
2455b71
6afeb40
7b062d0
bb21420
5995b12
4cc25ac
3badda9
c83a0c3
4e0cedf
7aaa48e
b936e7d
7752fda
aa809a3
176f539
0895277
a42a349
84c603d
9804605
b3374d3
96c9883
e95a0cb
a2eb745
13bb99a
c52b0ce
73a2112
6b828b1
5a1d00b
80339ac
7802bef
bd10b76
4d773f1
e7c3683
aa46ac8
2229f9f
ee939b6
b03ba72
9637109
2f17d48
a8bc403
93444e8
fb4551f
a32904c
b83961c
78cb1d2
6067df6
330e6ed
752df5e
d7fae90
f6ec4b6
6ba8236
a3df8ed
914aa7b
aa265f8
2f87cd5
cc2efaa
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing