OAI/NumberTheory/SiegelZeros/LocalAlgebra/ConePrimeLocalization.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W25.simple_baseChange_of_map_maximalIdeal line 30
  2. theorem OAI.SiegelZeros.WeightedTorusJets.W25.length_baseChange_of_flat_local line 49
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W25.finiteLength_baseChange_of_flat_local line 81
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W25.length_quotient_map_of_flat_local line 90
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W22.length_eq_of_semilinear_bijective line 108
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W22.quotient_length_eq_of_ringEquiv line 117
  7. theorem OAI.SiegelZeros.W17.ConeLocalLength.localized_maximalIdeal_map_eq line 147
  8. theorem OAI.SiegelZeros.W17.ConeLocalLength.localized_flat line 157
  9. abbrev OAI.SiegelZeros.W17.ConeLocalLength.polynomialPrime line 166
  10. theorem OAI.SiegelZeros.W17.ConeLocalLength.polynomialPrime_comap line 169
  11. instance OAI.SiegelZeros.W17.ConeLocalLength.polynomialPrime_liesOver line 183
  12. theorem OAI.SiegelZeros.W17.ConeLocalLength.polynomialLocal_flat line 186
  13. theorem OAI.SiegelZeros.W17.ConeLocalLength.polynomialLocal_maximalIdeal_map_eq line 190
  14. abbrev OAI.SiegelZeros.W17.ConeLocalLength.laurentPrime line 203
  15. instance OAI.SiegelZeros.W17.ConeLocalLength.laurent_polynomial_tower line 205
  16. theorem OAI.SiegelZeros.W17.ConeLocalLength.polynomialPrime_disjoint_powers_X line 210
  17. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentPrime_eq_map_polynomialPrime line 219
  18. instance OAI.SiegelZeros.W17.ConeLocalLength.laurentPrime_isPrime line 231
  19. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentPrime_comap line 237
  20. instance OAI.SiegelZeros.W17.ConeLocalLength.laurentPrime_liesOver line 250
  21. instance OAI.SiegelZeros.W17.ConeLocalLength.laurent_flat line 253
  22. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentLocal_flat line 258
  23. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentLocal_maximalIdeal_map_eq line 262
  24. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentLocal_quotient_length line 269
  25. abbrev OAI.SiegelZeros.W17.ConeLocalLength.AffineRing line 285
  26. abbrev OAI.SiegelZeros.W17.ConeLocalLength.ConeRing line 286
  27. abbrev OAI.SiegelZeros.W17.ConeLocalLength.ConeAway line 287
  28. abbrev OAI.SiegelZeros.W17.ConeLocalLength.LaurentChart line 288
  29. def OAI.SiegelZeros.W17.ConeLocalLength.coneHomogenizingUnit line 290
  30. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneHomogenizingUnit_val line 294
  31. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneHomogenizingUnit_inv_mul line 299
  32. def OAI.SiegelZeros.W17.ConeLocalLength.affineToConeAway line 305
  33. theorem OAI.SiegelZeros.W17.ConeLocalLength.affineToConeAway_C line 311
  34. theorem OAI.SiegelZeros.W17.ConeLocalLength.affineToConeAway_X line 316
  35. def OAI.SiegelZeros.W17.ConeLocalLength.coneToLaurent line 322
  36. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneToLaurent_C line 327
  37. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneToLaurent_X_none line 331
  38. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneToLaurent_X_some line 335
  39. def OAI.SiegelZeros.W17.ConeLocalLength.coneAwayToLaurent line 340
  40. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneAwayToLaurent_algebraMap line 344
  41. def OAI.SiegelZeros.W17.ConeLocalLength.laurentToConeAway line 348
  42. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentToConeAway_C line 351
  43. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentToConeAway_T line 355
  44. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentToConeAway_comp_coneToLaurent line 359
  45. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentToConeAway_comp_coneAwayToLaurent line 370
  46. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneAwayToLaurent_comp_affineToConeAway line 381
  47. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneAwayToLaurent_comp_laurentToConeAway line 401
  48. def OAI.SiegelZeros.W17.ConeLocalLength.coneLaurentEquiv line 418
  49. def OAI.SiegelZeros.WeightedTorusJets.W22.localPrimeTowerEquiv line 432
  50. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localPrimeTowerEquiv_algebraMap line 438
  51. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localPrimeTower_map_ideal line 445
  52. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localPrimeTower_quotient_length line 460
  53. theorem OAI.SiegelZeros.WeightedTorusJets.W22.primeCompl_map_eq_of_comap line 480
  54. def OAI.SiegelZeros.WeightedTorusJets.W22.primeLocalizationEquiv line 499
  55. theorem OAI.SiegelZeros.WeightedTorusJets.W22.primeLocalizationEquiv_map_ideal line 506
  56. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localized_quotient_length_eq_of_ringEquiv line 518
  57. def OAI.SiegelZeros.WeightedTorusJets.W22.MinimalParentsBelow line 539
  58. instance OAI.SiegelZeros.WeightedTorusJets.W22.minimalParentsBelow_fintype line 541
  59. instance OAI.SiegelZeros.WeightedTorusJets.W22.(instance at line 547) line 547
  60. def OAI.SiegelZeros.WeightedTorusJets.W22.localizedMinimalPrimesEquiv line 549
  61. theorem OAI.SiegelZeros.WeightedTorusJets.W22.localizedMinimalPrimesEquiv_apply line 576
  62. def OAI.SiegelZeros.W17.ConeLocalLength.awayChartPrime line 592
  63. instance OAI.SiegelZeros.W17.ConeLocalLength.awayChartPrime_isPrime line 595
  64. def OAI.SiegelZeros.W17.ConeLocalLength.conePrime line 599
  65. instance OAI.SiegelZeros.W17.ConeLocalLength.conePrime_isPrime line 602
  66. theorem OAI.SiegelZeros.W17.ConeLocalLength.homogenizing_coordinate_not_mem_conePrime line 606
  67. def OAI.SiegelZeros.W17.ConeLocalLength.conePrimeLocalizationEquiv line 616
  68. def OAI.SiegelZeros.W17.ConeLocalLength.affineLocalToConeLocal line 625
  69. def OAI.SiegelZeros.W17.ConeLocalLength.affineLocalConeAlgebra line 631
  70. theorem OAI.SiegelZeros.W17.ConeLocalLength.affineLocalToConeLocal_map_maximalIdeal line 635
  71. theorem OAI.SiegelZeros.W17.ConeLocalLength.affineLocalToConeLocal_flat line 645
  72. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneLocal_quotient_length line 659