OAI/NumberTheory/PiExponent/LocalAlgebra/CoordinateTranscendenceBasis.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.normalBasis_complement_surjective line 15
  2. theorem OAI.PiExponent.normalBasis_complement_injective line 49
  3. theorem OAI.PiExponent.polynomialGradient_mul line 88
  4. theorem OAI.PiExponent.polynomialGradient_rename line 98
  5. theorem OAI.PiExponent.pderiv_totalDegree_lt_of_pos line 123
  6. theorem OAI.PiExponent.eq_C_of_pderiv_eq_zero line 141
  7. theorem OAI.PiExponent.algebraicIndependent_of_pderiv_kernel line 162
  8. theorem OAI.PiExponent.normalBasis_complement_algebraicIndependent line 185
  9. theorem OAI.PiExponent.derivation_eq_zero_of_field_generators line 217
  10. theorem OAI.PiExponent.normalBasis_complement_isAlgebraic line 229
  11. theorem OAI.PiExponent.normalBasis_complement_isTranscendenceBasis line 278
  12. theorem OAI.PiExponent.polynomialResidueMap_field_generation line 302
  13. theorem OAI.PiExponent.primeNormalBasis_complement_isTranscendenceBasis line 318
  14. theorem OAI.PiExponent.idealResidueMap_field_generation line 331
  15. theorem OAI.PiExponent.idealResidueNormalBasis_complement_isTranscendenceBasis line 349