OAI/NumberTheory/SiegelZeros/Determinants/GenericNormalization.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.AlgebraicGeometry.Scheme.Hom.isIntegrallyClosed_stalk_normalization_of_field line 19
  2. def OAI.SiegelZeros.WeightedTorusJets.genericNormalization line 66
  3. def OAI.SiegelZeros.WeightedTorusJets.genericNormalizationMap line 69
  4. instance OAI.SiegelZeros.WeightedTorusJets.genericNormalization_isIntegral line 72
  5. instance OAI.SiegelZeros.WeightedTorusJets.genericNormalizationMap_isDominant line 76
  6. instance OAI.SiegelZeros.WeightedTorusJets.dominantFunctionFieldHom_isIso line 90
  7. def OAI.SiegelZeros.WeightedTorusJets.openImmersionFunctionFieldEquiv line 95
  8. def OAI.SiegelZeros.WeightedTorusJets.schemeBaseToStalk line 105
  9. abbrev OAI.SiegelZeros.WeightedTorusJets.schemeBaseStalkAlgebra line 109
  10. theorem OAI.SiegelZeros.WeightedTorusJets.schemeBaseToStalk_eq_global_germ line 113
  11. def OAI.SiegelZeros.WeightedTorusJets.dominantFunctionFieldAlgHom line 131
  12. def OAI.SiegelZeros.WeightedTorusJets.openImmersionFunctionFieldAlgEquiv line 158
  13. def OAI.SiegelZeros.WeightedTorusJets.normalizationFunctionFieldAlgHom line 169
  14. instance OAI.SiegelZeros.WeightedTorusJets.affineFunctionFieldAlgebra line 191
  15. theorem OAI.SiegelZeros.WeightedTorusJets.affineFunctionField_isScalarTower line 195
  16. def OAI.SiegelZeros.WeightedTorusJets.affineFractionFieldAlgEquiv line 210
  17. theorem OAI.SiegelZeros.WeightedTorusJets.isReduced_schemeImage line 235
  18. theorem OAI.SiegelZeros.WeightedTorusJets.isIntegral_schemeImage line 251
  19. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjEval line 267
  20. abbrev OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjChart line 271
  21. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjChartMap line 274
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjChartMap_mk line 280
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjEval_mem_chartMap_range line 294
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjChartMap_surjective line 312
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineProjChartMap_fromZero line 320
  26. def OAI.SiegelZeros.WeightedTorusJets.polynomialDegreeZeroEquiv line 343
  27. theorem OAI.SiegelZeros.WeightedTorusJets.polynomial_finiteType_degreeZero line 356
  28. def OAI.SiegelZeros.WeightedTorusJets.polynomialProjToSpec line 365
  29. theorem OAI.SiegelZeros.WeightedTorusJets.polynomialProjToSpec_isProper line 370
  30. def OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj line 389
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj_isImmersion line 396
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.affineIntoProj_toSpec line 405
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_proper_immersion_of_finiteType line 422
  34. instance OAI.SiegelZeros.WeightedTorusJets.schemeImage_isIntegral line 444
  35. instance OAI.SiegelZeros.WeightedTorusJets.schemeImage_isSeparated line 447
  36. theorem OAI.SiegelZeros.WeightedTorusJets.exists_normal_proper_model_of_finiteType_domain line 452