OAI/AlgebraicGeometry/Seshadri/Projective/HyperplaneAvoidance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.Projective.linearEquationLinear line 18
2. lemma OAI.MaximalSeshadri.Projective.linearEquation_single_one line 25
3. theorem OAI.MaximalSeshadri.Projective.exists_hyperplane_avoiding line 30
4. theorem OAI.MaximalSeshadri.Projective.exists_section_avoiding line 48