From ba9d416996cae7c823673be8080d713a7792bd58 Mon Sep 17 00:00:00 2001 From: teorth Date: Sun, 10 Dec 2023 09:29:44 -0800 Subject: [PATCH] Adding new lean files to main PFR.lean --- PFR.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/PFR.lean b/PFR.lean index bb6c7e60..59eafc7b 100644 --- a/PFR.lean +++ b/PFR.lean @@ -1,3 +1,4 @@ +import PFR.ApproxHomomorphism import PFR.Endgame import PFR.Entropy.Basic import PFR.Entropy.Group @@ -23,6 +24,7 @@ import PFR.ForMathlib.ProbabilityMeasureProdCont import PFR.ForMathlib.Uniform import PFR.Homomorphism import PFR.HundredPercent +import PFR.ImprovedPFR import PFR.Main import PFR.Mathlib.Algebra.Group.Hom.Basic import PFR.Mathlib.Algebra.Module.Submodule.Map