OAI/NumberTheory/PiExponent/Jets/PolynomialTangentDifferential.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.derivation_polynomial_map line 18
  2. def OAI.PiExponent.polynomialJacobian line 31
  3. def OAI.PiExponent.polynomialTangent line 37
  4. abbrev OAI.PiExponent.PolynomialNormal line 41
  5. theorem OAI.PiExponent.derivation_mem_polynomialTangent line 44
  6. theorem OAI.PiExponent.differential_relation_of_polynomialTangent line 53
  7. theorem OAI.PiExponent.logarithmic_differential_of_polynomialTangent line 65
  8. theorem OAI.PiExponent.differential_eq_zero_of_polynomialTangent line 79
  9. theorem OAI.PiExponent.polynomialNormal_span line 89
  10. abbrev OAI.PiExponent.PolynomialResidueField line 100
  11. def OAI.PiExponent.polynomialResidueMap line 103
  12. theorem OAI.PiExponent.polynomialResidueMap_eq_zero line 110
  13. theorem OAI.PiExponent.polynomialResidueMap_eq_zero_iff line 118
  14. theorem OAI.PiExponent.coordinate_sub_constant_mem_prime line 131
  15. theorem OAI.PiExponent.polynomialResidueField_essFiniteType line 138
  16. theorem OAI.PiExponent.constant_of_prime_polynomialTangent line 141