Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-23 23:08 aadd853d

View on Github →

feat(algebra/category): add more variants of Module.as_hom (#6822)

Estimated changes

Modified src/algebra/category/Module/basic.lean

added def Module.as_hom_left

added def Module.as_hom_right

added def linear_equiv.to_Module_iso'_left

added def linear_equiv.to_Module_iso'_right

Modified src/category_theory/sites/types.lean

Modified src/category_theory/types.lean