fix

leanprover-community · Oct 7, 2024 · 2bb78d0 · 2bb78d0
1 parent 65c8a3b
commit 2bb78d0
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Mathlib/RingTheory/FiniteLength.lean b/Mathlib/RingTheory/FiniteLength.lean
@@ -36,7 +36,8 @@ theorem LinearEquiv.isFiniteLength (e : M ≃ₗ[R] N)
     (h : IsFiniteLength R M) : IsFiniteLength R N := by
   induction' h with M _ _ _ M _ _ S _ _ ih generalizing N
   · have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
-  · have := IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
+  · have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
+      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
     exact .of_simple_quotient (ih <| e.submoduleMap S)
 
 variable (R M) in