OAI/NumberTheory/PiExponent/LocalAlgebra/ConeLocalLength.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.localized_maximalIdeal_map_eq line 22
  2. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.localized_flat line 32
  3. abbrev OAI.PiExponentSiegel.W17.ConeLocalLength.polynomialPrime line 41
  4. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.polynomialPrime_comap line 44
  5. instance OAI.PiExponentSiegel.W17.ConeLocalLength.polynomialPrime_liesOver line 58
  6. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.polynomialLocal_flat line 61
  7. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.polynomialLocal_maximalIdeal_map_eq line 65
  8. abbrev OAI.PiExponentSiegel.W17.ConeLocalLength.laurentPrime line 78
  9. instance OAI.PiExponentSiegel.W17.ConeLocalLength.laurent_polynomial_tower line 80
  10. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.polynomialPrime_disjoint_powers_X line 85
  11. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentPrime_eq_map_polynomialPrime line 94
  12. instance OAI.PiExponentSiegel.W17.ConeLocalLength.laurentPrime_isPrime line 106
  13. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentPrime_comap line 112
  14. instance OAI.PiExponentSiegel.W17.ConeLocalLength.laurentPrime_liesOver line 125
  15. instance OAI.PiExponentSiegel.W17.ConeLocalLength.laurent_flat line 128
  16. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentLocal_flat line 133
  17. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentLocal_maximalIdeal_map_eq line 137
  18. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentLocal_quotient_length line 144
  19. abbrev OAI.PiExponentSiegel.W17.ConeLocalLength.AffineRing line 159
  20. abbrev OAI.PiExponentSiegel.W17.ConeLocalLength.ConeRing line 160
  21. abbrev OAI.PiExponentSiegel.W17.ConeLocalLength.ConeAway line 161
  22. abbrev OAI.PiExponentSiegel.W17.ConeLocalLength.LaurentChart line 162
  23. def OAI.PiExponentSiegel.W17.ConeLocalLength.coneHomogenizingUnit line 164
  24. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneHomogenizingUnit_val line 168
  25. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneHomogenizingUnit_inv_mul line 173
  26. def OAI.PiExponentSiegel.W17.ConeLocalLength.affineToConeAway line 179
  27. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.affineToConeAway_C line 185
  28. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.affineToConeAway_X line 190
  29. def OAI.PiExponentSiegel.W17.ConeLocalLength.coneToLaurent line 196
  30. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneToLaurent_C line 201
  31. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneToLaurent_X_none line 205
  32. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneToLaurent_X_some line 209
  33. def OAI.PiExponentSiegel.W17.ConeLocalLength.coneAwayToLaurent line 214
  34. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneAwayToLaurent_algebraMap line 218
  35. def OAI.PiExponentSiegel.W17.ConeLocalLength.laurentToConeAway line 222
  36. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentToConeAway_C line 225
  37. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentToConeAway_T line 229
  38. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentToConeAway_comp_coneToLaurent line 233
  39. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.laurentToConeAway_comp_coneAwayToLaurent line 244
  40. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneAwayToLaurent_comp_affineToConeAway line 255
  41. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneAwayToLaurent_comp_laurentToConeAway line 275
  42. def OAI.PiExponentSiegel.W17.ConeLocalLength.coneLaurentEquiv line 292