fix(Algebra.Category.ModuleCat.Basic): remove `CoeOut (Submodule R M)…

… (ModuleCat R)` instance (#6032)
leanprover-community · Jul 29, 2023 · 061c9b8 · 061c9b8
1 parent b017d09
commit 061c9b8
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -379,6 +379,3 @@ theorem Iso.conj_eq_conj (i : X ≅ X') (f : End X) :
 end
 
 end ModuleCat
-
-instance (M : Type u) [AddCommGroup M] [Module R M] : CoeOut (Submodule R M) (ModuleCat R) :=
-  ⟨fun N => ModuleCat.of R N⟩