Add helper FunLike instance for AlgEquiv

leanprover-community · Nov 27, 2023 · d167b2b · d167b2b
1 parent 9b936db
commit d167b2b
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -109,6 +109,11 @@ instance : EquivLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
     obtain ⟨⟨g,_⟩,_⟩ := g
     congr
 
+/-- Helper instance since the coercion is not always found. -/
+instance : NDFunLike (A₁ ≃ₐ[R] A₂) A₁ A₂ where
+  coe := FunLike.coe
+  coe_injective' := FunLike.coe_injective'
+
 instance : AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂ where
   map_add f := f.map_add'
   map_mul f := f.map_mul'