OAI/NumberTheory/PiExponent/Jets/PrimeNormalCotangent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.extendModuleDerivation line 15
  2. theorem OAI.PiExponent.extendModuleDerivation_algebraMap line 26
  3. abbrev OAI.PiExponent.PrimeLocalCotangent line 41
  4. def OAI.PiExponent.primeResidueMap line 43
  5. def OAI.PiExponent.primeLocalPartial line 46
  6. theorem OAI.PiExponent.primeLocalPartial_polynomial line 54
  7. def OAI.PiExponent.primePartialNormal line 63
  8. def OAI.PiExponent.primeNormalPairing line 67
  9. def OAI.PiExponent.primePolynomialCotangent line 73
  10. theorem OAI.PiExponent.primeNormalPairing_polynomial line 79
  11. theorem OAI.PiExponent.primeNormalPairing_ker_le_tangent line 91
  12. def OAI.PiExponent.primeLocalDirectional line 101
  13. theorem OAI.PiExponent.primeNormalPairing_toCotangent line 106
  14. theorem OAI.PiExponent.primeNormalPairing_linearIndependent line 118
  15. theorem OAI.PiExponent.prime_cotangent_evaluation_surjective line 135