Adding new lean files to main PFR.lean

sgouezel · Dec 10, 2023 · ba9d416 · ba9d416
1 parent 6234e18
commit ba9d416
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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