OAI/NumberTheory/Jacobsthal/Siegel/GenericNormalization.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.AlgebraicGeometry.Scheme.Hom.isIntegrallyClosed_stalk_normalization_of_field line 22
  2. def OAI.Erdos970.WeightedTorusJets.genericNormalization line 69
  3. def OAI.Erdos970.WeightedTorusJets.genericNormalizationMap line 72
  4. instance OAI.Erdos970.WeightedTorusJets.genericNormalization_isIntegral line 75
  5. instance OAI.Erdos970.WeightedTorusJets.genericNormalizationMap_isDominant line 79
  6. instance OAI.Erdos970.WeightedTorusJets.dominantFunctionFieldHom_isIso line 93
  7. def OAI.Erdos970.WeightedTorusJets.openImmersionFunctionFieldEquiv line 98
  8. def OAI.Erdos970.WeightedTorusJets.schemeBaseToStalk line 108
  9. abbrev OAI.Erdos970.WeightedTorusJets.schemeBaseStalkAlgebra line 112
  10. theorem OAI.Erdos970.WeightedTorusJets.schemeBaseToStalk_eq_global_germ line 116
  11. def OAI.Erdos970.WeightedTorusJets.dominantFunctionFieldAlgHom line 134
  12. def OAI.Erdos970.WeightedTorusJets.openImmersionFunctionFieldAlgEquiv line 161
  13. def OAI.Erdos970.WeightedTorusJets.normalizationFunctionFieldAlgHom line 172
  14. instance OAI.Erdos970.WeightedTorusJets.affineFunctionFieldAlgebra line 194
  15. theorem OAI.Erdos970.WeightedTorusJets.affineFunctionField_isScalarTower line 198
  16. def OAI.Erdos970.WeightedTorusJets.affineFractionFieldAlgEquiv line 213
  17. theorem OAI.Erdos970.WeightedTorusJets.isReduced_schemeImage line 238
  18. theorem OAI.Erdos970.WeightedTorusJets.isIntegral_schemeImage line 254
  19. def OAI.Erdos970.WeightedTorusJets.Geometry.affineProjEval line 270
  20. abbrev OAI.Erdos970.WeightedTorusJets.Geometry.affineProjChart line 274
  21. def OAI.Erdos970.WeightedTorusJets.Geometry.affineProjChartMap line 277
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineProjChartMap_mk line 283
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineProjEval_mem_chartMap_range line 297
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineProjChartMap_surjective line 315
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineProjChartMap_fromZero line 323
  26. def OAI.Erdos970.WeightedTorusJets.polynomialDegreeZeroEquiv line 346
  27. theorem OAI.Erdos970.WeightedTorusJets.polynomial_finiteType_degreeZero line 359
  28. def OAI.Erdos970.WeightedTorusJets.polynomialProjToSpec line 368
  29. theorem OAI.Erdos970.WeightedTorusJets.polynomialProjToSpec_isProper line 373
  30. def OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj line 392
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj_isImmersion line 399
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.affineIntoProj_toSpec line 408
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_proper_immersion_of_finiteType line 425
  34. instance OAI.Erdos970.WeightedTorusJets.schemeImage_isIntegral line 447
  35. instance OAI.Erdos970.WeightedTorusJets.schemeImage_isSeparated line 450
  36. theorem OAI.Erdos970.WeightedTorusJets.exists_normal_proper_model_of_finiteType_domain line 455