OAI/AlgebraicGeometry/Seshadri/Sheaves/ClosedPushforwardEuler.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.ClosedPushforward.scalar_naturality line 20
2. theorem OAI.MaximalSeshadri.ClosedPushforward.complexLinearPushforward line 27
3. lemma OAI.MaximalSeshadri.ClosedPushforward.cohomologyMap_base_smul line 43
4. def OAI.MaximalSeshadri.ClosedPushforward.cohomologyLinearMap line 56
5. lemma OAI.MaximalSeshadri.ClosedPushforward.cohomologyLinearMap_eq line 68
6. def OAI.MaximalSeshadri.ClosedPushforward.cohomologyEquiv line 71
7. theorem OAI.MaximalSeshadri.ClosedPushforward.euler_pushforward line 78