OAI/AlgebraicGeometry/Seshadri/Bertini/LinearForms.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.BertiniIntegral.linear_saturated line 14
2. lemma OAI.MaximalSeshadri.BertiniIntegral.linear_pow_saturated line 31
3. theorem OAI.MaximalSeshadri.BertiniIntegral.linear_ideal_isPrime line 41
4. def OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm line 94
5. def OAI.MaximalSeshadri.BertiniIntegral.separateLinearVariable line 97
6. lemma OAI.MaximalSeshadri.BertiniIntegral.separateLinearVariable_coeff_one line 102
7. lemma OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_regular_of_unit line 113
8. theorem OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_regular line 127
9. lemma OAI.MaximalSeshadri.BertiniIntegral.separateLinearVariable_eq line 165
10. theorem OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_saturated line 182
11. theorem OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_isPrime_of_unit line 210
12. theorem OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_isPrime line 240
13. theorem OAI.MaximalSeshadri.BertiniIntegral.universalHyperplane_isDomain line 283
14. theorem OAI.MaximalSeshadri.BertiniIntegral.flat_tensor_map_injective line 297
15. theorem OAI.MaximalSeshadri.BertiniIntegral.flat_baseChange_domain_of_injective line 304
16. theorem OAI.MaximalSeshadri.BertiniIntegral.geometricGeneric_domain_of_injective line 312
17. theorem OAI.MaximalSeshadri.BertiniIntegral.geometricGeneric_domain_of_nonempty_localization line 321