OAI/AlgebraicGeometry/Seshadri/Blowup/OrderContraction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.PlaneBlowup.chartExponent line 12
2. lemma OAI.MaximalSeshadri.PlaneBlowup.chartExponent_apply line 22
3. lemma OAI.MaximalSeshadri.PlaneBlowup.chartExponent_injective line 25
4. lemma OAI.MaximalSeshadri.PlaneBlowup.chartExponent_self line 32
5. lemma OAI.MaximalSeshadri.PlaneBlowup.chartSubstitution_eq_mapDomain line 38
6. lemma OAI.MaximalSeshadri.PlaneBlowup.chartSubstitution_injective line 66
7. lemma OAI.MaximalSeshadri.PlaneBlowup.variable_pow_dvd_iff line 70
8. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_coeff line 87
9. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_coeff_outside line 93
10. lemma OAI.MaximalSeshadri.PlaneBlowup.substitution_variable_pow_dvd_iff line 99
11. lemma OAI.MaximalSeshadri.PlaneBlowup.chart_exceptional_pow_dvd_iff line 113
12. theorem OAI.MaximalSeshadri.FlatContraction.contraction line 137
13. def OAI.MaximalSeshadri.PlaneBlowup.exceptionalChartIdeal line 177
14. lemma OAI.MaximalSeshadri.PlaneBlowup.exceptionalChart_comap_pow line 180
15. lemma OAI.MaximalSeshadri.PlaneBlowup.flat_chart_order line 189
16. lemma OAI.MaximalSeshadri.IdealPullback.comap_pow line 212
17. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_pow line 232
18. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_of_affine_equation line 247
19. lemma OAI.MaximalSeshadri.InvertibleLocal.invertible_Spec_of_span_regular line 259
20. lemma OAI.MaximalSeshadri.IdealPullback.specIdeal_map line 278
21. lemma OAI.MaximalSeshadri.FlatContraction.includeRight_flat line 302