OAI/NumberTheory/PiExponent/Ampleness/ExceptionalAffineChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ExceptionalAffineChart.chartOpen line 16
2. def OAI.PiExponent.ExceptionalAffineChart.affineGammaEquiv line 19
3. def OAI.PiExponent.ExceptionalAffineChart.chartFunctionsEquiv line 23
4. def OAI.PiExponent.ExceptionalAffineChart.chartPowerIdeal line 26
5. theorem OAI.PiExponent.ExceptionalAffineChart.chartPowerIdeal_eq line 30
6. theorem OAI.PiExponent.ExceptionalAffineChart.map_chartPowerIdeal line 48
7. def OAI.PiExponent.ExceptionalAffineChart.idealMapAddEquiv line 79
8. def OAI.PiExponent.ExceptionalAffineChart.sectionsEquiv line 91
9. theorem OAI.PiExponent.ExceptionalAffineChart.sectionsEquiv_apply line 100
10. def OAI.PiExponent.ExceptionalAffineChart.idealChartFrame line 109