OAI/NumberTheory/SiegelZeros/LocalAlgebra/TriangularLocalParametersTransport.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.W08.coordinatePolynomialSplit line 25
  2. def OAI.SiegelZeros.W08.coordinateCoefficientSplit line 29
  3. theorem OAI.SiegelZeros.W08.coordinateCoefficientSplit_X_zero line 34
  4. theorem OAI.SiegelZeros.W08.coordinateCoefficientSplit_X_succ line 38
  5. theorem OAI.SiegelZeros.W08.coordinateCoefficientSplit_C line 42
  6. theorem OAI.SiegelZeros.W08.coordinateCoefficientSplit_aeval line 46
  7. def OAI.SiegelZeros.W08.coordinateMinpolyIdeal line 59
  8. theorem OAI.SiegelZeros.W08.coordinateMinpolyIdeal_map line 63
  9. def OAI.SiegelZeros.W08.coefficientAdjoinRootQuotientEquiv line 70
  10. theorem OAI.SiegelZeros.W08.coefficientAdjoinRootQuotientEquiv_mk line 77
  11. def OAI.SiegelZeros.W08.coordinateMinpolyQuotientEquiv line 84
  12. theorem OAI.SiegelZeros.W08.coordinateMinpolyQuotientEquiv_mk line 91
  13. theorem OAI.SiegelZeros.W08.coordinateMinpolyQuotientEquiv_X_zero line 97
  14. theorem OAI.SiegelZeros.W08.coordinateMinpolyQuotientEquiv_X_succ line 103
  15. theorem OAI.SiegelZeros.W08.coordinateMinpolyQuotientEquiv_C line 109
  16. theorem OAI.SiegelZeros.W08.coordinateMinpolyIdeal_le_of_mem_contraction line 115
  17. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.scalar_top_eq_principal line 135
  18. def OAI.SiegelZeros.W10.TriangularLocalParameters.principalModuleQuotientEquiv line 139
  19. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.principalModuleQuotientEquiv_mk line 144
  20. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.regular_cons_of_principal_kernel line 152
  21. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.ofList_cons_eq_comap line 172
  22. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.lift_parameters line 179
  23. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.regular_element_of_ne_zero line 195
  24. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.singleton_parameter_regular line 198
  25. def OAI.SiegelZeros.W10.TriangularLocalParameters.firstPolynomial line 212
  26. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstPolynomial_ne_zero line 214
  27. def OAI.SiegelZeros.W10.TriangularLocalParameters.firstLocalParameter line 219
  28. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstLocalParameter_ne_zero line 222
  29. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstLocalParameter_span line 226
  30. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.oneVariable_parameters line 240
  31. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.zeroVariable_maximal_eq_bot line 255
  32. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.zeroVariable_parameters line 266
  33. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.maximal_coefficient_contraction line 282
  34. def OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinateContraction line 290
  35. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinateContraction_isMaximal line 293
  36. def OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinatePolynomial line 308
  37. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinatePolynomial_irreducible line 311
  38. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinatePolynomial_mem line 319
  39. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinateIdeal_le line 324
  40. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.firstCoordinateRelation_ne_zero line 329
  41. def OAI.SiegelZeros.W23.quotientParameterPrime line 347
  42. instance OAI.SiegelZeros.W23.quotientParameterPrime_isPrime line 350
  43. instance OAI.SiegelZeros.W23.quotientParameterPrime_isMaximal line 356
  44. theorem OAI.SiegelZeros.W23.mem_quotientParameterPrime_mk line 362
  45. def OAI.SiegelZeros.W23.parameterLocalizedIdeal line 366
  46. def OAI.SiegelZeros.W23.parameterLocalizationMap line 372
  47. theorem OAI.SiegelZeros.W23.parameterLocalizationMap_algebraMap line 382
  48. theorem OAI.SiegelZeros.W23.parameterLocalizedIdeal_le_ker line 388
  49. def OAI.SiegelZeros.W23.parameterLocalQuotientForward line 396
  50. theorem OAI.SiegelZeros.W23.parameterLocalQuotientForward_mk line 403
  51. def OAI.SiegelZeros.W23.parameterQuotientToLocalQuotient line 407
  52. theorem OAI.SiegelZeros.W23.parameterQuotientToLocalQuotient_mk line 414
  53. theorem OAI.SiegelZeros.W23.parameterQuotientToLocalQuotient_units line 419
  54. def OAI.SiegelZeros.W23.parameterLocalQuotientReverse line 433
  55. theorem OAI.SiegelZeros.W23.parameterLocalQuotientReverse_algebraMap line 440
  56. theorem OAI.SiegelZeros.W23.parameterLocalQuotient_reverse_forward line 446
  57. theorem OAI.SiegelZeros.W23.parameterLocalQuotient_forward_reverse line 457
  58. def OAI.SiegelZeros.W23.localizationQuotientParametersEquiv line 468
  59. theorem OAI.SiegelZeros.W23.localizationQuotientParametersEquiv_mk_algebraMap line 478
  60. theorem OAI.SiegelZeros.W23.parameterLocalQuotient_isLocalRing line 487
  61. theorem OAI.SiegelZeros.W23.localizationQuotientParametersEquiv_maximalIdeal line 491
  62. def OAI.SiegelZeros.W23.localizationQuotientParametersResidueEquiv line 499
  63. theorem OAI.SiegelZeros.W23.localizationQuotientParametersResidueEquiv_residue line 506
  64. theorem OAI.SiegelZeros.W23.parameterLocalizedIdeal_span_singleton line 518
  65. theorem OAI.SiegelZeros.W23.atPrimeImage_comap line 529
  66. def OAI.SiegelZeros.W23.atPrimeEquivOfRingEquiv line 535
  67. theorem OAI.SiegelZeros.W23.atPrimeEquivOfRingEquiv_algebraMap line 540
  68. def OAI.SiegelZeros.W23.localizationQuotientParametersEquivTrans line 548
  69. theorem OAI.SiegelZeros.W23.localizationQuotientParametersEquivTrans_mk_algebraMap line 554
  70. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.polynomialMaximal_regularParameters line 573
  71. theorem OAI.SiegelZeros.W23.intrinsic_length_eq_of_ringEquiv line 621
  72. theorem OAI.SiegelZeros.W23.quotient_module_length_eq_intrinsic line 633
  73. theorem OAI.SiegelZeros.W23.parameterLocalizationMap_surjective line 640
  74. theorem OAI.SiegelZeros.W23.quotient_localized_length_eq line 647
  75. theorem OAI.SiegelZeros.W23.quotient_localized_length_eq_explicit line 662
  76. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.regular_map_ringEquiv line 678
  77. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.regularParameters_transport line 686
  78. theorem OAI.SiegelZeros.W10.TriangularLocalParameters.polynomialMaximal_regularParameters_of_ringEquiv line 698