chore: update Frobenius to reflect new mathlib PR.

ImperialCollegeLondon · Dec 18, 2024 · 227d04e · 227d04e
1 parent b6ba352
commit 227d04e
Show file tree

Hide file tree

Showing 5 changed files with 2 additions and 2,162 deletions.
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -33,9 +33,6 @@ import FLT.Mathlib.Data.ENNReal.Inv
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler
 import FLT.MathlibExperiments.Coalgebra.TensorProduct
-import FLT.MathlibExperiments.Frobenius
-import FLT.MathlibExperiments.Frobenius2
-import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsCentralSimple
 import FLT.MathlibExperiments.IsFrobenius