fix (LinearAlgebra.Dual): delete instFunLikeDual (#6637)

It seems that Lean can find `LinearMap.instFunLike` just fine now. Furthermore, `Module.Dual.instFunLikeDual` was causing TC synthesis to fail. We delete it.
leanprover-community · Aug 18, 2023 · 971fb7a · 971fb7a
1 parent 05ef5b4
commit 971fb7a
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean
@@ -124,9 +124,6 @@ namespace Dual
 
 instance : Inhabited (Dual R M) := ⟨0⟩
 
-instance : FunLike (Dual R M) M fun _ => R :=
-  inferInstanceAs (FunLike (M →ₗ[R] R) M fun _ => R)
-
 /-- Maps a module M to the dual of the dual of M. See `Module.erange_coe` and
 `Module.evalEquiv`. -/
 def eval : M →ₗ[R] Dual R (Dual R M) :=