Theorem SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app

Modification history

2026-02-12 12:31
Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean
feat(Algebra/Category): `IsQuasicoherent` from a cover (#35168)
Added SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_appView on Github →