fix

leanprover-community · Feb 5, 2025 · 28b9bc8 · 28b9bc8
1 parent edd8a79
commit 28b9bc8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RepresentationTheory/Invariants.lean b/Mathlib/RepresentationTheory/Invariants.lean
@@ -183,7 +183,7 @@ instance : (invariantsFunctor k G).Additive where
 
 /-- The adjunction between the functor equipping a module with the trivial representation, and
 the functor sending a representation to its submodule of invariants. -/
-noncomputable abbrev invariantsAdjunction : trivialFunctor ⊣ invariantsFunctor k G :=
+noncomputable abbrev invariantsAdjunction : trivialFunctor G ⊣ invariantsFunctor k G :=
   Adjunction.mkOfHomEquiv {
     homEquiv := fun _ _ => {
       toFun := fun f => ModuleCat.ofHom <|