OAI/AlgebraicGeometry/Seshadri/Jets/PolynomialJets.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MaximalSeshadri.AlgebraicJets.JetIndex line 16
  2. instance OAI.MaximalSeshadri.AlgebraicJets.jetIndexFinite line 18
  3. def OAI.MaximalSeshadri.AlgebraicJets.polynomialJetCoeffs line 21
  4. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialJetCoeffs_ker line 26
  5. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialJetCoeffs_surjective line 35
  6. def OAI.MaximalSeshadri.AlgebraicJets.polynomialJetEquiv line 50
  7. def OAI.MaximalSeshadri.AlgebraicJets.polynomialTranslate line 56
  8. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialTranslate_constantCoeff line 62
  9. lemma OAI.MaximalSeshadri.AlgebraicJets.idealOfVars_eq_ker_constantCoeff line 71
  10. theorem OAI.MaximalSeshadri.AlgebraicJets.mem_rationalPoint_pow_iff line 82
  11. def OAI.MaximalSeshadri.AlgebraicJets.polynomialJetCoeffsAt line 106
  12. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialJetCoeffsAt_ker line 110
  13. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialJetCoeffsAt_surjective line 119
  14. def OAI.MaximalSeshadri.AlgebraicJets.polynomialJetEquivAt line 123
  15. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialJetEquivAt_mk line 129
  16. lemma OAI.MaximalSeshadri.AlgebraicJets.polynomialJetEquiv_mk line 134
  17. abbrev OAI.MaximalSeshadri.AlgebraicJets.JetAlgebra line 146
  18. def OAI.MaximalSeshadri.AlgebraicJets.jetAugment line 149
  19. lemma OAI.MaximalSeshadri.AlgebraicJets.jetAugment_mk line 155
  20. lemma OAI.MaximalSeshadri.AlgebraicJets.jetAugment_surjective line 160
  21. lemma OAI.MaximalSeshadri.AlgebraicJets.jetAugment_ker line 164
  22. lemma OAI.MaximalSeshadri.AlgebraicJets.jetAugment_ker_nilpotent line 182
  23. lemma OAI.MaximalSeshadri.AlgebraicJets.exists_lift_with_coordinates line 196
  24. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_regular_taylor line 219
  25. lemma OAI.MaximalSeshadri.AlgebraicJets.map_idealOfVars line 251
  26. def OAI.MaximalSeshadri.AlgebraicJets.mapJetAlgebra line 262
  27. lemma OAI.MaximalSeshadri.AlgebraicJets.mapJetAlgebra_mk line 269
  28. lemma OAI.MaximalSeshadri.AlgebraicJets.jetAugment_map line 273
  29. lemma OAI.MaximalSeshadri.AlgebraicJets.jetAugment_ker_pow line 279