OAI/NumberTheory/Jacobsthal/Siegel/FiniteTypeFieldModelEquiv.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finiteTypeFieldModel_isFractionRing line 18
  2. def OAI.Erdos970.WeightedTorusJets.Geometry.finiteTypeFieldModelEquiv line 26
  3. theorem OAI.Erdos970.WeightedTorusJets.exists_normal_proper_model_of_essFiniteType_field line 40
  4. theorem OAI.Erdos970.WeightedTorusJets.scheme_global_germ_isIntegral line 72
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isAlgebraic_of_logarithmicForm_eq_zero line 93
  6. def OAI.Erdos970.WeightedTorusJets.Geometry.derivationOnIdeal line 123
  7. def OAI.Erdos970.WeightedTorusJets.Geometry.derivationCotangent line 132
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.derivationCotangentResidue line 142
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.independent_functionals_surjective line 152
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_ideal_element_with_derivatives line 161
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.invariantDerivation_X line 183
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localize_invariantDerivation_X line 188
  13. def OAI.Erdos970.WeightedTorusJets.Geometry.derivationAmbientCovector line 205
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationAmbientCovector_tmul_D line 210
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.derivationAmbientCovector_conormal line 215
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.range_conormalDifferential line 220
  17. def OAI.Erdos970.WeightedTorusJets.Geometry.residueTangentMap line 231
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.residueTangentMap_tmul_D line 238
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ker_conormalDual_eq_range_residueTangent line 247
  20. def OAI.Erdos970.WeightedTorusJets.Geometry.normalQuotientEquivCotangentDual line 255
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.normalQuotientEquivCotangentDual_mk line 267
  22. def OAI.Erdos970.WeightedTorusJets.Geometry.localizedPolynomialKaehlerBasis line 283
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localizedPolynomialKaehlerBasis_apply line 288
  24. def OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicKaehlerBasis line 293
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicKaehlerBasis_apply line 299
  26. def OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicAmbientEquiv line 308
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicAmbientEquiv_apply line 314
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicAmbientEquiv_residueTangentMap line 339
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.logarithmicAmbientEquiv_invariantDerivation line 349
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.map_range_residueTangent_logarithmic line 367
  31. def OAI.Erdos970.WeightedTorusJets.Geometry.coordinateNormalEquivCotangentDual line 378
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateNormalEquivCotangentDual_mk line 390
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateNormal_invariant_pairing line 399
  34. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_basis_ker_dotProduct_algebraMap line 417
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_normal_image_at_point line 455
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_independent_image_finset line 465
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_normal_image_eq_min line 485
  38. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_independent_normal_finset line 503