chore(algebra/category/Module): remove unnecessary universe restricti…

…on (#12610) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Mar 12, 2022 · a4187fe · a4187fe
1 parent 31d28c6
commit a4187fe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/algebra/category/Module/basic.lean b/src/algebra/category/Module/basic.lean
@@ -109,7 +109,7 @@ rfl
 rfl
 
 /-- Typecheck a `linear_map` as a morphism in `Module R`. -/
-def of_hom {R : Type u} [ring R] {X Y : Type u} [add_comm_group X] [module R X] [add_comm_group Y]
+def of_hom {R : Type u} [ring R] {X Y : Type v} [add_comm_group X] [module R X] [add_comm_group Y]
   [module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y := f
 
 instance : has_zero (Module R) := ⟨of R punit⟩