From dbfc54e7d14e31427275d3036cb302a57c618c18 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 14 Sep 2023 15:50:25 +0900
Subject: [PATCH] rm spuirous parentheses

---
 theories/hoelder.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/hoelder.v b/theories/hoelder.v
index d00f61f27..2d262c10f 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -47,7 +47,7 @@ Definition Lnorm p f :=
   | p%:E => if p == 0%R then
               mu (f @^-1` (setT `\ 0%R))
             else
-              ((\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1)
+              (\int[mu]_x (`|f x| `^ p)%:E) `^ p^-1
   | +oo => if mu [set: T] > 0 then ess_sup mu (normr \o f) else 0
   | -oo => 0
   end.