OAI/NumberTheory/PiExponent/LocalAlgebra/CoordinateFiniteSlice.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.CoordinateFiniteSlice.coordinateEquiv line 14
  2. theorem OAI.PiExponent.CoordinateFiniteSlice.coordinateEquiv_inl line 19
  3. theorem OAI.PiExponent.CoordinateFiniteSlice.coordinateEquiv_inr line 22
  4. def OAI.PiExponent.CoordinateFiniteSlice.coordinateRenaming line 25
  5. theorem OAI.PiExponent.CoordinateFiniteSlice.coordinateRenaming_X_inl line 29
  6. theorem OAI.PiExponent.CoordinateFiniteSlice.coordinateRenaming_X_inr line 36
  7. abbrev OAI.PiExponent.CoordinateFiniteSlice.splitPrime line 43
  8. instance OAI.PiExponent.CoordinateFiniteSlice.splitPrime_isPrime line 47
  9. def OAI.PiExponent.CoordinateFiniteSlice.residueEquiv line 50
  10. theorem OAI.PiExponent.CoordinateFiniteSlice.residueEquiv_coordinate_inl line 54
  11. theorem OAI.PiExponent.CoordinateFiniteSlice.residueEquiv_coordinate_inr line 63
  12. theorem OAI.PiExponent.CoordinateFiniteSlice.complementary_transcendenceBasis line 71
  13. theorem OAI.PiExponent.CoordinateFiniteSlice.splitPrime_mem_minimalPrimes line 79
  14. def OAI.PiExponent.CoordinateFiniteSlice.residueCoordinates line 92
  15. def OAI.PiExponent.CoordinateFiniteSlice.slicePoint line 95
  16. theorem OAI.PiExponent.CoordinateFiniteSlice.enumeratedSliceMap_X_inl line 98
  17. theorem OAI.PiExponent.CoordinateFiniteSlice.enumeratedSliceMap_X_inr line 106
  18. theorem OAI.PiExponent.CoordinateFiniteSlice.residueEquiv_symm_coordinate_inl line 113
  19. theorem OAI.PiExponent.CoordinateFiniteSlice.residueEquiv_symm_coordinate_inr line 122