OAI/NumberTheory/Jacobsthal/Siegel/DominantFunctionFieldHom.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.existsUnique_globalSection_scalar line 29
  2. theorem OAI.Erdos970.WeightedTorusJets.genericPoint_eq_of_isDominant line 41
  3. def OAI.Erdos970.WeightedTorusJets.dominantFunctionFieldHom line 48
  4. theorem OAI.Erdos970.WeightedTorusJets.germToFunctionField_dominantFunctionFieldHom line 53
  5. theorem OAI.Erdos970.WeightedTorusJets.isDominant_fromSpecStalk_genericPoint line 65
  6. theorem OAI.Erdos970.WeightedTorusJets.finite_integralClosure_of_normal_subring line 83
  7. theorem OAI.Erdos970.WeightedTorusJets.finite_integralClosure_of_finiteType_charZero line 103
  8. theorem OAI.Erdos970.WeightedTorusJets.isFractionRing_genericPoint_preimage_sections line 118
  9. theorem OAI.Erdos970.WeightedTorusJets.isFinite_genericNormalization line 148
  10. theorem OAI.Erdos970.isDiscreteValuationRing_of_fraction_pole line 186
  11. theorem OAI.Erdos970.height_eq_one_of_prime_denominator line 230
  12. theorem OAI.Erdos970.mem_algebraMap_of_mem_height_one_localizations line 274
  13. theorem OAI.Erdos970.AlgebraicGeometry.Scheme.isDiscreteValuationRing_stalk_of_isIntegrallyClosed line 336
  14. theorem OAI.Erdos970.AlgebraicGeometry.Scheme.exists_stalk_unit_of_ord_eq_zero line 351
  15. theorem OAI.Erdos970.AlgebraicGeometry.IsAffineOpen.isIntegrallyClosed_of_stalks line 370
  16. theorem OAI.Erdos970.AlgebraicGeometry.IsAffineOpen.exists_section_of_codim_one_regular line 381
  17. theorem OAI.Erdos970.AlgebraicGeometry.Scheme.exists_global_unit_of_stalk_units line 426
  18. theorem OAI.Erdos970.AlgebraicGeometry.Scheme.exists_global_unit_of_ord_eq_zero line 481