OAI/AlgebraicGeometry/Seshadri/Projective/HyperplaneIdeal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.IdealPullback.vanishingIdeal_comap_open line 18
2. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_support line 36
3. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_radical_eq line 44
4. lemma OAI.MaximalSeshadri.IdealPullback.vanishingIdeal_open_chart line 55
5. lemma OAI.MaximalSeshadri.Projective.chart_linear_equation_radical line 82
6. def OAI.MaximalSeshadri.Projective.ambientHyperplane line 105
7. lemma OAI.MaximalSeshadri.Projective.ambientHyperplane_chart line 108