OAI/AlgebraicGeometry/Seshadri/Blowup/SchemeHartogs.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.Hartogs.variable_pow_dvd_iff line 16
2. lemma OAI.MaximalSeshadri.Hartogs.power_variable_dvd_other_mul line 33
3. lemma OAI.MaximalSeshadri.Hartogs.mem_smul_top_iff_dvd line 42
4. lemma OAI.MaximalSeshadri.Hartogs.polynomial_power_sequence line 47
5. lemma OAI.MaximalSeshadri.Hartogs.flat_power_sequence line 59
6. lemma OAI.MaximalSeshadri.Hartogs.flat_cancel_other_coordinate line 67
7. theorem OAI.MaximalSeshadri.Hartogs.flat_hartogs line 80
8. lemma OAI.MaximalSeshadri.Hartogs.functionField_restrict line 127
9. lemma OAI.MaximalSeshadri.Hartogs.basicOpen_nonempty line 134
10. lemma OAI.MaximalSeshadri.Hartogs.coordinate_denominator line 138
11. theorem OAI.MaximalSeshadri.Hartogs.affine_hartogs line 164
12. lemma OAI.MaximalSeshadri.Hartogs.open_appTop_injective line 219
13. lemma OAI.MaximalSeshadri.Hartogs.restrict_topIso line 230
14. theorem OAI.MaximalSeshadri.Hartogs.blowup_descend line 235