OAI/NumberTheory/PiExponent/Analysis/AlgebraicLogarithmicObstruction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.extendDerivation line 16
  2. theorem OAI.PiExponent.extendDerivation_algebraMap line 24
  3. def OAI.PiExponent.ratFuncDerivative line 34
  4. theorem OAI.PiExponent.ratFuncDerivative_X line 40
  5. theorem OAI.PiExponent.finite_extension_no_logarithmic_differential line 48
  6. theorem OAI.PiExponent.adjoin_finite_no_logarithmic_differential line 69
  7. theorem OAI.PiExponent.logarithmic_differential_base_change line 91
  8. theorem OAI.PiExponent.no_logarithmic_differential_over_intermediateField line 99
  9. theorem OAI.PiExponent.isAlgebraic_of_logarithmic_differential line 108
  10. theorem OAI.PiExponent.constant_of_logarithmic_differential line 117