OAI/NumberTheory/SiegelZeros/LocalAlgebra/ParameterIdeal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.transcendental_of_nonzero_nonunit line 23
  2. theorem OAI.SiegelZeros.WeightedTorusJets.residue_aeval_eq_eval_zero line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.isUnit_aeval_of_eval_zero_ne_zero line 39
  4. abbrev OAI.SiegelZeros.WeightedTorusJets.parameterIdeal line 46
  5. instance OAI.SiegelZeros.WeightedTorusJets.parameterIdeal_isPrime line 49
  6. abbrev OAI.SiegelZeros.WeightedTorusJets.parameterRing line 52
  7. theorem OAI.SiegelZeros.WeightedTorusJets.exists_parameter_local_algebra line 54
  8. theorem OAI.SiegelZeros.WeightedTorusJets.formallySmooth_of_flat_of_essFiniteType_of_map_maximalIdeal line 93
  9. theorem OAI.SiegelZeros.WeightedTorusJets.formallySmooth_of_essFiniteType_of_discreteValuationRing line 113
  10. def OAI.SiegelZeros.WeightedTorusJets.Geometry.conormalDifferential line 141
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conormalDifferential_toCotangent line 149
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conormalDifferential_injective line 157
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_derivation_residue_eq_one line 166
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.uniformizer_cotangent_ne_zero line 190
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_transverse_derivation_uniformizer line 201
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.localizeDerivation line 219
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.localizeDerivation_algebraMap line 227
  18. theorem OAI.SiegelZeros.WeightedTorusJets.int_coefficients_eq_zero_of_sum_eq_zero line 243
  19. theorem OAI.SiegelZeros.WeightedTorusJets.exists_unit_mul_zpow_order line 250
  20. theorem OAI.SiegelZeros.WeightedTorusJets.log_deriv_mul_zpow line 273
  21. theorem OAI.SiegelZeros.WeightedTorusJets.exists_rescaled_log_deriv_lift line 282
  22. theorem OAI.SiegelZeros.WeightedTorusJets.sum_orders_eq_zero_of_kaehler_relation line 300
  23. theorem OAI.SiegelZeros.WeightedTorusJets.scheme_residue_equation_of_log_form line 333
  24. theorem OAI.SiegelZeros.WeightedTorusJets.schemeBaseStalkAlgebra_essFiniteType line 388
  25. theorem OAI.SiegelZeros.WeightedTorusJets.schemeBaseStalkAlgebra_isScalarTower line 401
  26. theorem OAI.SiegelZeros.WeightedTorusJets.scheme_residue_equation_of_locallyOfFiniteType line 425
  27. theorem OAI.SiegelZeros.WeightedTorusJets.scheme_orders_zero_of_locallyOfFiniteType_log_form line 448
  28. theorem OAI.SiegelZeros.WeightedTorusJets.scheme_global_units_of_locallyOfFiniteType_log_form line 469