Revert analysis/normed_space/inner_product

leanprover-community · Sep 5, 2021 · bdc242b · bdc242b
1 parent bfab166
commit bdc242b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/analysis/normed_space/inner_product.lean b/src/analysis/normed_space/inner_product.lean
@@ -379,7 +379,7 @@ end
 variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 local notation `IK` := @is_R_or_C.I 𝕜 _
-local notation `absR` := abs
+local notation `absR` := has_abs.abs
 local notation `absK` := @is_R_or_C.abs 𝕜 _
 local postfix `†`:90 := @is_R_or_C.conj 𝕜 _
 local postfix `⋆`:90 := complex.conj