OAI/AlgebraicGeometry/Seshadri/Intersection/FiniteLineEuler.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.FiniteSupport.finite_line_pushforward_euler line 20
2. theorem OAI.MaximalSeshadri.FiniteSupport.finite_line_pushforward_finiteDimensional line 31
3. theorem OAI.MaximalSeshadri.FiniteSupport.finite_line_euler_eq_sum_stalks line 48