FLT_files update

ImperialCollegeLondon · Dec 3, 2024 · ded579b · ded579b
1 parent d0ed977
commit ded579b
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -10,6 +10,7 @@ import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
 import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.ForMathlib.MiscLemmas
+import FLT.ForMathlib.Topology.Algebra.Algebra
 import FLT.FromMathlib.Algebra
 import FLT.GaloisRepresentation.Cyclotomic
 import FLT.GaloisRepresentation.HardlyRamified
@@ -20,6 +21,9 @@ import FLT.HIMExperiments.flatness
 import FLT.HaarMeasure.ConcreteCharCalculations
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Hard.Results
+import FLT.Mathlib.Algebra.Algebra.Subalgebra.Pi
+import FLT.Mathlib.Algebra.Group.Subgroup.Defs
+import FLT.Mathlib.Algebra.Group.Units.Hom
 import FLT.Mathlib.Algebra.Order.Hom.Monoid
 import FLT.Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
 import FLT.Mathlib.Analysis.Complex.Basic