Def SheafOfModules.unitToPushforwardObjUnit

Modification history

2025-11-19 06:07
Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean
chore: move Mathlib to the module system (#31786) …
Deleted SheafOfModules.unitToPushforwardObjUnitView on Github →
2025-11-08 15:24
Mathlib/Algebra/Category/ModuleCat/Sheaf/PullbackFree.lean
feat(Algebra/Category/ModuleCat/Sheaf): `O_S ⟶ f_* O_X` and `f^* O_S ≅ O_X` (#30398)
Added SheafOfModules.unitToPushforwardObjUnitView on Github →