OAI/NumberTheory/PiExponent/LocalAlgebra/SeparablePointLength.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.SeparablePointLength.coefficientBaseChangeEquiv line 14
  2. theorem OAI.PiExponent.SeparablePointLength.coefficientExtension_flat line 18
  3. theorem OAI.PiExponent.SeparablePointLength.coefficientExtension_finite line 22
  4. theorem OAI.PiExponent.SeparablePointLength.coefficientExtension_unramified line 26
  5. theorem OAI.PiExponent.SeparablePointLength.length_quotient_map_of_unramified line 31
  6. def OAI.PiExponent.SeparablePointLength.contractedPoint line 43
  7. instance OAI.PiExponent.SeparablePointLength.contractedPoint_isPrime line 46
  8. instance OAI.PiExponent.SeparablePointLength.point_liesOver line 50
  9. theorem OAI.PiExponent.SeparablePointLength.contractedPoint_eq_ker line 53
  10. def OAI.PiExponent.SeparablePointLength.pointLocalMap line 60
  11. def OAI.PiExponent.SeparablePointLength.pointLocalAlgebra line 66
  12. theorem OAI.PiExponent.SeparablePointLength.pointLocal_flat line 71
  13. theorem OAI.PiExponent.SeparablePointLength.pointLocal_unramified line 79
  14. theorem OAI.PiExponent.SeparablePointLength.pointLocal_essFiniteType line 88
  15. theorem OAI.PiExponent.SeparablePointLength.pointLocalMap_algebraMap line 96
  16. instance OAI.PiExponent.SeparablePointLength.pointLocalMap_isLocalHom line 102
  17. theorem OAI.PiExponent.SeparablePointLength.pointLocalMap_ideal_map line 106
  18. theorem OAI.PiExponent.SeparablePointLength.pointLocal_quotient_length line 117
  19. theorem OAI.PiExponent.SeparablePointLength.point_mem_minimalPrimes_map line 138