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