OAI/NumberTheory/PiExponent/LocalAlgebra/CoordinateSliceLength.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.CoordinateSliceLength.localizedLength line 16
  2. theorem OAI.PiExponent.CoordinateSliceLength.localizedLength_congr line 20
  3. def OAI.PiExponent.CoordinateSliceLength.rationalizePolynomial line 30
  4. theorem OAI.PiExponent.CoordinateSliceLength.rationalizePolynomial_X_inl line 36
  5. theorem OAI.PiExponent.CoordinateSliceLength.rationalizePolynomial_X_inr line 40
  6. theorem OAI.PiExponent.CoordinateSliceLength.closedPolynomialIdeal_eq_ker line 46
  7. theorem OAI.PiExponent.CoordinateSliceLength.map_prime_eq_closedPolynomialIdeal line 56
  8. theorem OAI.PiExponent.CoordinateSliceLength.closedPolynomialIdeal_comap line 69
  9. theorem OAI.PiExponent.CoordinateSliceLength.closedPolynomialIdeal_mem_minimalPrimes line 80
  10. theorem OAI.PiExponent.CoordinateSliceLength.polynomialPrimeClosedPointEquiv_algebraMap line 96
  11. theorem OAI.PiExponent.CoordinateSliceLength.polynomialPrimeClosedPointEquiv_map_ideal line 113
  12. theorem OAI.PiExponent.CoordinateSliceLength.length_eq_rationalized line 126
  13. theorem OAI.PiExponent.CoordinateSliceLength.splitCoefficientResidue_isScalarTower line 135
  14. theorem OAI.PiExponent.CoordinateSliceLength.splitResidue_finite line 147
  15. def OAI.PiExponent.CoordinateSliceLength.slicePoint line 159
  16. def OAI.PiExponent.CoordinateSliceLength.residueSlice line 163
  17. theorem OAI.PiExponent.CoordinateSliceLength.map_rationalize_eq_residueSlice line 169
  18. theorem OAI.PiExponent.CoordinateSliceLength.closedPolynomialIdeal_eq_contractedPoint line 196
  19. theorem OAI.PiExponent.CoordinateSliceLength.length_eq_residueSlice line 207
  20. theorem OAI.PiExponent.CoordinateSliceLength.slicePoint_mem_minimalPrimes line 235