OAI/AlgebraicGeometry/Seshadri/Bertini/GeometricDomains.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.BertiniIntegral.finite_self_tensor_dimension_one line 13
2. theorem OAI.MaximalSeshadri.BertiniIntegral.relative_algebraic_closure_of_self_tensor_domain line 28
3. lemma OAI.MaximalSeshadri.BertiniIntegral.monic_factor_descends line 46
4. theorem OAI.MaximalSeshadri.BertiniIntegral.irreducible_map_of_relative_closure line 56
5. def OAI.MaximalSeshadri.BertiniIntegral.rootBaseChangeEquiv line 79
6. theorem OAI.MaximalSeshadri.BertiniIntegral.finite_separable_tensor_isDomain line 92
7. lemma OAI.MaximalSeshadri.BertiniIntegral.tensor_sum_in_intermediate_range line 112
8. theorem OAI.MaximalSeshadri.BertiniIntegral.separable_tensor_isDomain line 122
9. theorem OAI.MaximalSeshadri.BertiniIntegral.tensorProduct_isDomain_general line 171
10. theorem OAI.MaximalSeshadri.BertiniIntegral.self_tensor_domain_geometrically_domain line 210
11. theorem OAI.MaximalSeshadri.BertiniIntegral.tensor_localization_isDomain line 242
12. theorem OAI.MaximalSeshadri.BertiniIntegral.fraction_self_tensor_isDomain line 271
13. theorem OAI.MaximalSeshadri.BertiniIntegral.self_tensor_domain_geometrically_domain_algebra line 289