OAI/NumberTheory/SiegelZeros/Structure/FiniteTypeFieldModelEquiv.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finiteTypeFieldModel_isFractionRing line 14
  2. def OAI.SiegelZeros.WeightedTorusJets.Geometry.finiteTypeFieldModelEquiv line 22
  3. theorem OAI.SiegelZeros.WeightedTorusJets.exists_normal_proper_model_of_essFiniteType_field line 36
  4. theorem OAI.SiegelZeros.WeightedTorusJets.scheme_global_germ_isIntegral line 68
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isAlgebraic_of_logarithmicForm_eq_zero line 89
  6. def OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationOnIdeal line 119
  7. def OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationCotangent line 128
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationCotangentResidue line 138
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.independent_functionals_surjective line 148
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_ideal_element_with_derivatives line 157
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantDerivation_X line 176
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localize_invariantDerivation_X line 181
  13. def OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationAmbientCovector line 198
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationAmbientCovector_tmul_D line 203
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.derivationAmbientCovector_conormal line 208
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.range_conormalDifferential line 213
  17. def OAI.SiegelZeros.WeightedTorusJets.Geometry.residueTangentMap line 224
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.residueTangentMap_tmul_D line 231
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ker_conormalDual_eq_range_residueTangent line 240
  20. def OAI.SiegelZeros.WeightedTorusJets.Geometry.normalQuotientEquivCotangentDual line 248
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.normalQuotientEquivCotangentDual_mk line 260
  22. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizedPolynomialKaehlerBasis line 276
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localizedPolynomialKaehlerBasis_apply line 281
  24. def OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicKaehlerBasis line 286
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicKaehlerBasis_apply line 292
  26. def OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicAmbientEquiv line 301
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicAmbientEquiv_apply line 307
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicAmbientEquiv_residueTangentMap line 330
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.logarithmicAmbientEquiv_invariantDerivation line 340
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.map_range_residueTangent_logarithmic line 358
  31. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateNormalEquivCotangentDual line 369
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateNormalEquivCotangentDual_mk line 381
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateNormal_invariant_pairing line 390
  34. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_basis_ker_dotProduct_algebraMap line 408
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_normal_image_at_point line 446
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_independent_image_finset line 456
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_normal_image_eq_min line 476
  38. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_independent_normal_finset line 494