OAI/AlgebraicGeometry/Seshadri/Analytic/CoordinateJets.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticFirst line 16
  2. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticSecond line 17
  3. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticFormal_first line 19
  4. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticFormal_second line 31
  5. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticPullback line 45
  6. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor line 54
  7. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor_constantCoeff line 59
  8. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor_affineFirst line 67
  9. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor_affineSecond line 81
  10. lemma OAI.MaximalSeshadri.AlgebraicJets.jetChart_unique line 106
  11. def OAI.MaximalSeshadri.AlgebraicJets.formalTrunc line 126
  12. lemma OAI.MaximalSeshadri.AlgebraicJets.formalTrunc_augment line 129
  13. lemma OAI.MaximalSeshadri.AlgebraicJets.formalTrunc_polynomial line 134
  14. theorem OAI.MaximalSeshadri.AlgebraicJets.formalTaylor_detects_ideal_power line 141
  15. theorem OAI.MaximalSeshadri.AlgebraicJets.formalTaylor_injective line 164
  16. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor_coordinates line 202
  17. theorem OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor_detects_ideal_power line 220
  18. theorem OAI.MaximalSeshadri.AnalyticCoordinates.analyticTaylor_injective line 231