diff --git a/Mathlib/RingTheory/Regular/RegularSequence.lean b/Mathlib/RingTheory/Regular/RegularSequence.lean index 5477dd102ec5b..8f2d5b1dc7f21 100644 --- a/Mathlib/RingTheory/Regular/RegularSequence.lean +++ b/Mathlib/RingTheory/Regular/RegularSequence.lean @@ -5,6 +5,7 @@ Authors: Brendan Murphy -/ import Mathlib.RingTheory.Regular.IsSMulRegular import Mathlib.RingTheory.Artinian +import Mathlib.RingTheory.Nakayama import Mathlib.Logic.Equiv.TransferInstance import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic