OAI/Algebra/FrobeniusObstruction/FrobeniusRing.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.Frobenius.Series line 13
  2. def OAI.BoundaryOnly.FormalObstruction.Frobenius.powerIdeal line 15
  3. abbrev OAI.BoundaryOnly.FormalObstruction.Frobenius.Ring line 18
  4. def OAI.BoundaryOnly.FormalObstruction.Frobenius.Good line 20
  5. def OAI.BoundaryOnly.FormalObstruction.Frobenius.cut line 22
  6. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coeff_cut line 25
  7. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.cut_empty line 29
  8. def OAI.BoundaryOnly.FormalObstruction.Frobenius.tail line 35
  9. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coeff_tail line 39
  10. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.one_coordinate_decomposition line 43
  11. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.cut_insert line 53
  12. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.subtract_cut_mem line 59
  13. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coeff_ideal_eq_zero line 72
  14. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mem_powerIdeal_iff line 82
  15. def OAI.BoundaryOnly.FormalObstruction.Frobenius.quotientCoeff line 96
  16. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.quotientCoeff_mk line 103
  17. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.quotient_ext line 107
  18. abbrev OAI.BoundaryOnly.FormalObstruction.Frobenius.Box line 117
  19. def OAI.BoundaryOnly.FormalObstruction.Frobenius.exponent line 119
  20. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.exponent_apply line 123
  21. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.exponent_good line 127
  22. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.exponent_injective line 132
  23. def OAI.BoundaryOnly.FormalObstruction.Frobenius.boxOfGood line 139
  24. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.exponent_boxOfGood line 143
  25. def OAI.BoundaryOnly.FormalObstruction.Frobenius.monomial line 149
  26. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.quotientCoeff_monomial line 152
  27. def OAI.BoundaryOnly.FormalObstruction.Frobenius.coefficients line 158
  28. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coefficients_apply line 162
  29. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coefficients_injective line 166
  30. def OAI.BoundaryOnly.FormalObstruction.Frobenius.fromCoefficients line 174
  31. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coefficients_fromCoefficients line 177
  32. def OAI.BoundaryOnly.FormalObstruction.Frobenius.coefficientEquiv line 183
  33. instance OAI.BoundaryOnly.FormalObstruction.Frobenius.moduleFinite_quotient line 188
  34. instance OAI.BoundaryOnly.FormalObstruction.Frobenius.moduleFree_quotient line 191
  35. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.monomial_expansion line 194
  36. def OAI.BoundaryOnly.FormalObstruction.Frobenius.topExponent line 199
  37. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topExponent_apply line 203
  38. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topExponent_good line 207
  39. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.good_le_top line 213
  40. def OAI.BoundaryOnly.FormalObstruction.Frobenius.topMonomial line 220
  41. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topMonomial_coefficient line 224
  42. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topMonomial_ne_zero line 230
  43. def OAI.BoundaryOnly.FormalObstruction.Frobenius.constantHom line 237
  44. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.constantHom_mk line 243
  45. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.topMonomial_mul line 246
  46. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.constantHom_algebraMap line 265
  47. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.algebraMap_injective line 271
  48. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.quotient_charP line 276
  49. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.monomial_power_zero line 281
  50. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.frobenius_zero_of_constant line 302
  51. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.series_frobenius_mem line 318
  52. def OAI.BoundaryOnly.FormalObstruction.Frobenius.nilpotentSubst line 331
  53. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.has_nilpotentSubst line 335
  54. def OAI.BoundaryOnly.FormalObstruction.Frobenius.nilpotentEval line 340
  55. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.nilpotentEval_X line 350
  56. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.isNilpotent_of_powers line 358
  57. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.nilpotentEval_zero_on_powerIdeal line 362
  58. def OAI.BoundaryOnly.FormalObstruction.Frobenius.eval line 372
  59. def OAI.BoundaryOnly.FormalObstruction.Frobenius.coordinate line 377
  60. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.coordinate_pow line 381
  61. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.eval_coordinate line 387
  62. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.monomial_eq_prod line 393
  63. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.algHom_ext line 399
  64. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.eval_self line 409
  65. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.pderiv_powerIdeal line 422
  66. def OAI.BoundaryOnly.FormalObstruction.Frobenius.partialDeriv line 435
  67. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_mk line 443
  68. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_coordinate line 449
  69. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.series_pderiv_commute line 457
  70. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.partial_commute line 468
  71. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.residue_partial_zero line 475