OAI/AlgebraicGeometry/Seshadri/Analytic/FormalSeries.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.AnalyticCoordinates.absolute_add line 17
  2. lemma OAI.MaximalSeshadri.AnalyticCoordinates.seriesEval_add line 27
  3. lemma OAI.MaximalSeshadri.AnalyticCoordinates.eventually_polydisk line 35
  4. lemma OAI.MaximalSeshadri.AnalyticCoordinates.common_absolute_radius line 41
  5. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_add line 50
  6. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_mul line 63
  7. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_const line 77
  8. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficientLinear line 93
  9. abbrev OAI.MaximalSeshadri.AnalyticCoordinates.BiSeries line 124
  10. def OAI.MaximalSeshadri.AnalyticCoordinates.biCoeff line 126
  11. def OAI.MaximalSeshadri.AnalyticCoordinates.biSeries line 128
  12. lemma OAI.MaximalSeshadri.AnalyticCoordinates.biCoeff_biSeries line 131
  13. lemma OAI.MaximalSeshadri.AnalyticCoordinates.biCoeff_injective line 134
  14. lemma OAI.MaximalSeshadri.AnalyticCoordinates.biCoeff_mul line 142
  15. def OAI.MaximalSeshadri.AnalyticCoordinates.analyticFormal line 168
  16. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_congr line 202
  17. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticFormal_congr line 208
  18. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticFormal_constantCoeff line 212
  19. lemma OAI.MaximalSeshadri.AnalyticCoordinates.analyticCoefficients_monomial line 217
  20. def OAI.MaximalSeshadri.FormalCoordinates.powerSeriesMapEquiv line 241
  21. lemma OAI.MaximalSeshadri.FormalCoordinates.powerSeriesMapEquiv_coeff line 247
  22. def OAI.MaximalSeshadri.FormalCoordinates.binaryEquiv line 252
  23. lemma OAI.MaximalSeshadri.FormalCoordinates.binaryEquiv_coeff line 258
  24. lemma OAI.MaximalSeshadri.FormalCoordinates.binaryEquiv_X_zero line 266
  25. lemma OAI.MaximalSeshadri.FormalCoordinates.binaryEquiv_X_one line 270
  26. lemma OAI.MaximalSeshadri.FormalCoordinates.binaryEquiv_constantCoeff line 280