OAI/AlgebraicGeometry/Seshadri/Configurations/SmoothRationalPoints.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.algebraic_of_countable_presentation line 14
2. theorem OAI.MaximalSeshadri.point_of_countable_presentation line 31
3. theorem OAI.MaximalSeshadri.point_avoiding_sequence_of_countable_presentation line 47
4. theorem OAI.MaximalSeshadri.point_avoiding_sequence line 90
5. theorem OAI.MaximalSeshadri.rational_point_outside_countable_closed line 99
6. lemma OAI.MaximalSeshadri.smooth_positive_dimension_nontrivial_kernel line 132
7. theorem OAI.MaximalSeshadri.smooth_affine_uncountable_rational_points line 152
8. theorem OAI.MaximalSeshadri.rational_kernel_injective line 173
9. def OAI.MaximalSeshadri.fieldPoint line 191
10. theorem OAI.MaximalSeshadri.smooth_scheme_uncountable_rational_points line 194