Theorem SheafOfModules.ιFree_mapFree_inv

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.ιFree_mapFree_invView 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.ιFree_mapFree_invView on Github →