OAI/AlgebraicGeometry/Seshadri/Bertini/CountableSpecialization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.BertiniIntegral.field_embedding_over_countable line 12
2. theorem OAI.MaximalSeshadri.BertiniIntegral.generic_field_embedding line 35
3. theorem OAI.MaximalSeshadri.BertiniIntegral.integral_specialization_of_countable_model line 48
4. theorem OAI.MaximalSeshadri.BertiniIntegral.countable_etale_hyperplane_integral_equation line 81
5. theorem OAI.MaximalSeshadri.BertiniIntegral.hyperplaneFamily_geometricGeneric_of_injective line 133
6. theorem OAI.MaximalSeshadri.BertiniIntegral.countable_hyperplane_integral_equation line 161
7. theorem OAI.MaximalSeshadri.BertiniIntegral.hyperplane_injective_descent line 217
8. def OAI.MaximalSeshadri.BertiniIntegral.polynomialQuotientBaseChange line 266
9. theorem OAI.MaximalSeshadri.BertiniIntegral.countable_polynomial_model line 283
10. lemma OAI.MaximalSeshadri.BertiniIntegral.polynomialQuotientBaseChange_tmul line 315
11. theorem OAI.MaximalSeshadri.BertiniIntegral.countable_model_with_elements line 321