fix name

pygae · Jul 17, 2023 · 1c375e9 · 1c375e9
1 parent 7e94d7c
commit 1c375e9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/geometric_algebra/from_mathlib/category_theory.lean b/src/geometric_algebra/from_mathlib/category_theory.lean
@@ -49,7 +49,7 @@ instance concrete_category : concrete_category.{v} (QuadraticModule.{v} R) :=
 { forget := { obj := λ R, R, map := λ R S f, (f : R → S) },
   forget_faithful := { } }
 
-instance has_forget_to_AddCommGroup : has_forget₂ (QuadraticModule R) (Module R) :=
+instance has_forget_to_Module : has_forget₂ (QuadraticModule R) (Module R) :=
 { forget₂ :=
   { obj := λ M, Module.of R M,
     map := λ M₁ M₂ f, isometric_map.to_linear_map f } }