OAI/AlgebraicGeometry/Seshadri/Analytic/PolynomialCharts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.AlgebraicJets.polynomialDifferential line 15
  2. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialDifferential_C line 18
  3. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialDifferential_add line 23
  4. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialDifferential_mul line 29
  5. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialDifferential_X line 37
  6. theorem OAI.MaximalSeshadri.AlgebraicJets.hasFDerivAt_polynomialEval line 43
  7. theorem OAI.MaximalSeshadri.AlgebraicJets.analyticAt_polynomial_eval line 53
  8. def OAI.MaximalSeshadri.AlgebraicJets.augmentedLinear line 69
  9. lemma OAI.MaximalSeshadri.AlgebraicJets.augmentedLinear_apply line 74
  10. theorem OAI.MaximalSeshadri.AlgebraicJets.augmentedLinear_bijective line 77
  11. theorem OAI.MaximalSeshadri.AlgebraicJets.submersive_jacobian_at_point line 116
  12. def OAI.MaximalSeshadri.AlgebraicJets.augmentedPolynomial line 150
  13. def OAI.MaximalSeshadri.AlgebraicJets.augmentedDerivative line 154
  14. lemma OAI.MaximalSeshadri.AlgebraicJets.augmentedPolynomial_hasFDerivAt line 159
  15. lemma OAI.MaximalSeshadri.AlgebraicJets.augmentedPolynomial_analyticAt line 174
  16. def OAI.MaximalSeshadri.AlgebraicJets.augmentedDerivativeEquiv line 179
  17. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_analytic_augmented_inverse line 187