Theorem SheafOfModules.map_ιFree_mapFree_hom

Modification history

2026-04-24 19:21

Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

refactor(Algebra/Category/ModuleCat/Sheaf/Free): generalize `SheafOfModules.mapFree` (#38341) …

Deleted SheafOfModules.map_ιFree_mapFree_hom View on Github →

2025-12-18 09:28

Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of `Presentation` (#32437) …

Added SheafOfModules.map_ιFree_mapFree_hom View on Github →