Skip to content

Commit c3a4078

Browse files
kbuzzardkbuzzard
committed
don't need the ore localization algebra import yet, move elsewhere
1 parent 6f33c8d commit c3a4078

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

‎FLT/MathlibExperiments/FrobeniusRiou.lean

-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ import Mathlib.RingTheory.Ideal.Over
1313
import Mathlib.FieldTheory.Normal
1414
import Mathlib
1515
import Mathlib.RingTheory.OreLocalization.Ring
16-
import FLT.ForMathlib.Algebra
1716

1817
/-!
1918

0 commit comments

Comments
 (0)