We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0f2df1b commit 888e200Copy full SHA for 888e200
1 file changed
Mathlib/Analysis/NormedSpace/ENormedSpace.lean
@@ -34,8 +34,6 @@ normed space, extended norm
34
35
noncomputable section
36
37
-set_option linter.deprecated false
38
-
39
open ENNReal
40
41
/-- Extended norm on a vector space. As in the case of normed spaces, we require only
0 commit comments