OAI/NumberTheory/Jacobsthal/Siegel/ParameterIdeal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.transcendental_of_nonzero_nonunit line 26
  2. theorem OAI.Erdos970.WeightedTorusJets.residue_aeval_eq_eval_zero line 32
  3. theorem OAI.Erdos970.WeightedTorusJets.isUnit_aeval_of_eval_zero_ne_zero line 42
  4. abbrev OAI.Erdos970.WeightedTorusJets.parameterIdeal line 49
  5. instance OAI.Erdos970.WeightedTorusJets.parameterIdeal_isPrime line 52
  6. abbrev OAI.Erdos970.WeightedTorusJets.parameterRing line 55
  7. theorem OAI.Erdos970.WeightedTorusJets.exists_parameter_local_algebra line 57
  8. theorem OAI.Erdos970.WeightedTorusJets.formallySmooth_of_flat_of_essFiniteType_of_map_maximalIdeal line 96
  9. theorem OAI.Erdos970.WeightedTorusJets.formallySmooth_of_essFiniteType_of_discreteValuationRing line 116
  10. def OAI.Erdos970.WeightedTorusJets.Geometry.conormalDifferential line 144
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conormalDifferential_toCotangent line 152
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conormalDifferential_injective line 160
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_derivation_residue_eq_one line 169
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.uniformizer_cotangent_ne_zero line 193
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_transverse_derivation_uniformizer line 204
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.localizeDerivation line 222
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.localizeDerivation_algebraMap line 230
  18. theorem OAI.Erdos970.WeightedTorusJets.int_coefficients_eq_zero_of_sum_eq_zero line 246
  19. theorem OAI.Erdos970.WeightedTorusJets.exists_unit_mul_zpow_order line 253
  20. theorem OAI.Erdos970.WeightedTorusJets.log_deriv_mul_zpow line 276
  21. theorem OAI.Erdos970.WeightedTorusJets.exists_rescaled_log_deriv_lift line 285
  22. theorem OAI.Erdos970.WeightedTorusJets.sum_orders_eq_zero_of_kaehler_relation line 303
  23. theorem OAI.Erdos970.WeightedTorusJets.scheme_residue_equation_of_log_form line 336
  24. theorem OAI.Erdos970.WeightedTorusJets.schemeBaseStalkAlgebra_essFiniteType line 391
  25. theorem OAI.Erdos970.WeightedTorusJets.schemeBaseStalkAlgebra_isScalarTower line 404
  26. theorem OAI.Erdos970.WeightedTorusJets.scheme_residue_equation_of_locallyOfFiniteType line 428
  27. theorem OAI.Erdos970.WeightedTorusJets.scheme_orders_zero_of_locallyOfFiniteType_log_form line 451
  28. theorem OAI.Erdos970.WeightedTorusJets.scheme_global_units_of_locallyOfFiniteType_log_form line 472