Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 11:37 a4187fef

View on Github →

chore(algebra/category/Module): remove unnecessary universe restriction (#12610)

Estimated changes

modified def Module.of_hom