From 9131997c1e7ca0d9cc6689ec0b4e03fa2c7f995c Mon Sep 17 00:00:00 2001 From: LorenzoLuccioli Date: Fri, 5 Apr 2024 13:58:48 +0200 Subject: [PATCH] remove useless comment --- TestingLowerBounds/KullbackLeibler.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/TestingLowerBounds/KullbackLeibler.lean b/TestingLowerBounds/KullbackLeibler.lean index d3954af9..5cc744d8 100644 --- a/TestingLowerBounds/KullbackLeibler.lean +++ b/TestingLowerBounds/KullbackLeibler.lean @@ -157,8 +157,6 @@ end kl_nonneg section Conditional variable {β : Type*} {mβ : MeasurableSpace β} --- variable {κ η : kernel α β} - open Classical in