Commit 2023-04-11 12:30 f5a903bb

View on Github →

feat: port Algebra.Category.Module.Basic (#3260)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Basic.lean

added def CategoryTheory.Iso.toLinearEquiv

added def LinearEquiv.toModuleIso

added theorem ModuleCat.Iso.conj_eq_conj

added theorem ModuleCat.Iso.homCongr_eq_arrowCongr

added def ModuleCat.asHom

added def ModuleCat.asHomLeft

added def ModuleCat.asHomRight

added theorem ModuleCat.coe_comp

added theorem ModuleCat.coe_of

added theorem ModuleCat.comp_def

added theorem ModuleCat.forget₂_map

added theorem ModuleCat.forget₂_obj

added theorem ModuleCat.forget₂_obj_moduleCat_of

added theorem ModuleCat.hom_ext

added theorem ModuleCat.id_apply

added theorem ModuleCat.isZero_of_subsingleton

added def ModuleCat.of

added def ModuleCat.ofHom

added theorem ModuleCat.ofHom_apply

added def ModuleCat.ofSelfIso

added structure ModuleCat

added def linearEquivIsoModuleIso