Theorem SheafOfModules.map_ιFree_mapFreeIso_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) …
Added SheafOfModules.map_ιFree_mapFreeIso_invView on Github →