OAI/NumberTheory/SiegelZeros/Structure/DominantFunctionFieldHom.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.existsUnique_globalSection_scalar line 26
  2. theorem OAI.SiegelZeros.WeightedTorusJets.genericPoint_eq_of_isDominant line 38
  3. def OAI.SiegelZeros.WeightedTorusJets.dominantFunctionFieldHom line 45
  4. theorem OAI.SiegelZeros.WeightedTorusJets.germToFunctionField_dominantFunctionFieldHom line 50
  5. theorem OAI.SiegelZeros.WeightedTorusJets.isDominant_fromSpecStalk_genericPoint line 62
  6. theorem OAI.SiegelZeros.WeightedTorusJets.finite_integralClosure_of_normal_subring line 80
  7. theorem OAI.SiegelZeros.WeightedTorusJets.finite_integralClosure_of_finiteType_charZero line 100
  8. theorem OAI.SiegelZeros.WeightedTorusJets.isFractionRing_genericPoint_preimage_sections line 115
  9. theorem OAI.SiegelZeros.WeightedTorusJets.isFinite_genericNormalization line 145
  10. theorem OAI.SiegelZeros.isDiscreteValuationRing_of_fraction_pole line 183
  11. theorem OAI.SiegelZeros.height_eq_one_of_prime_denominator line 227
  12. theorem OAI.SiegelZeros.mem_algebraMap_of_mem_height_one_localizations line 271
  13. theorem OAI.SiegelZeros.AlgebraicGeometry.Scheme.isDiscreteValuationRing_stalk_of_isIntegrallyClosed line 333
  14. theorem OAI.SiegelZeros.AlgebraicGeometry.Scheme.exists_stalk_unit_of_ord_eq_zero line 348
  15. theorem OAI.SiegelZeros.AlgebraicGeometry.IsAffineOpen.isIntegrallyClosed_of_stalks line 367
  16. theorem OAI.SiegelZeros.AlgebraicGeometry.IsAffineOpen.exists_section_of_codim_one_regular line 378
  17. theorem OAI.SiegelZeros.AlgebraicGeometry.Scheme.exists_global_unit_of_stalk_units line 423
  18. theorem OAI.SiegelZeros.AlgebraicGeometry.Scheme.exists_global_unit_of_ord_eq_zero line 478