diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean index 42ba499019caf..e4e118895ecbc 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean @@ -360,7 +360,8 @@ section /-! `Subalgebra`s inherit structure from their `Submodule` coercions. -/ -instance module' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : Module R' S := +instance (priority := low) module' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : + Module R' S := S.toSubmodule.module' #align subalgebra.module' Subalgebra.module'