Update Mathlib/Algebra/Azumaya/Defs.lean

Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · Jan 22, 2025 · de74508 · de74508
1 parent 0d72d72
commit de74508
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Algebra/Azumaya/Defs.lean b/Mathlib/Algebra/Azumaya/Defs.lean
@@ -38,7 +38,7 @@ noncomputable abbrev instModuleTensorProductMop :
 /-- The canonical map from `A ⊗[R] Aᵐᵒᵖ` to `Module.End R A` where
   `a ⊗ b` maps to `f : x ↦ a * x * b`. -/
 noncomputable abbrev AlgHom.tensorMopToEnd : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A :=
-  letI := instModuleTensorProductMop R A
+  letI : Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
   letI : IsScalarTower R (A ⊗[R] Aᵐᵒᵖ) A := {
     smul_assoc := fun r ab a ↦ by
       change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _