Commit 2024-02-06 07:03 d78efd06
View on Github →chore(NormedSpace/Basic): move some theorems to NormedSpace.Real
(#10206)
This way we don't switch between general normed spaces and real normed spaces
back and forth throughout the file.
chore(NormedSpace/Basic): move some theorems to NormedSpace.Real
(#10206)
This way we don't switch between general normed spaces and real normed spaces
back and forth throughout the file.