Update Mathlib.lean

leanprover-community · Oct 7, 2024 · 65c8a3b · 65c8a3b
1 parent 1695fa1
commit 65c8a3b
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3886,6 +3886,7 @@ import Mathlib.RingTheory.EssentialFiniteness
 import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Filtration
+import Mathlib.RingTheory.FiniteLength
 import Mathlib.RingTheory.FinitePresentation
 import Mathlib.RingTheory.FiniteStability
 import Mathlib.RingTheory.FiniteType