diff --git a/Mathlib/Algebra/Lie/Quotient.lean b/Mathlib/Algebra/Lie/Quotient.lean index e6ae53a34c3e9..367d16adeac24 100644 --- a/Mathlib/Algebra/Lie/Quotient.lean +++ b/Mathlib/Algebra/Lie/Quotient.lean @@ -43,7 +43,7 @@ instance : HasQuotient M (LieSubmodule R L M) := namespace Quotient -variable {N I} +variable {N} instance addCommGroup : AddCommGroup (M ⧸ N) := Submodule.Quotient.addCommGroup _