OAI/NumberTheory/PiExponent/Approximation/CoordinateSliceComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.CoordinateSliceComparison.primeLength line 16
2. theorem OAI.PiExponent.CoordinateSliceComparison.splitBasis line 21
3. theorem OAI.PiExponent.CoordinateSliceComparison.map_residueSlice_eq_enumeratedSliceMap line 28
4. theorem OAI.PiExponent.CoordinateSliceComparison.map_splitPoint_eq line 58
5. theorem OAI.PiExponent.CoordinateSliceComparison.map_slice_ideal line 66
6. theorem OAI.PiExponent.CoordinateSliceComparison.length_eq_enumeratedSlice line 75
7. theorem OAI.PiExponent.CoordinateSliceComparison.slicePoint_mem_minimalPrimes line 92
8. theorem OAI.PiExponent.CoordinateSliceComparison.length_eq_enumeratedSlice_of_normalBasis line 108
9. theorem OAI.PiExponent.CoordinateSliceComparison.slicePoint_mem_minimalPrimes_of_normalBasis line 119
10. theorem OAI.PiExponent.CoordinateSliceComparison.map_span_sliceFamily line 132
11. theorem OAI.PiExponent.CoordinateSliceComparison.length_eq_sliceFamily_of_normalBasis line 142
12. theorem OAI.PiExponent.CoordinateSliceComparison.sliceFamily_mem_minimalPrimes_of_normalBasis line 157