OAI/RingTheory/Multiplicity/RootTowerRemainderExponent.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.RootTower.remainderExponent line 12
  2. lemma OAI.Lech.RootTower.remainderExponent_apply line 16
  3. def OAI.Lech.RootTower.exponentRemainder line 20
  4. def OAI.Lech.RootTower.exponentQuotient line 23
  5. lemma OAI.Lech.RootTower.exponent_split line 26
  6. lemma OAI.Lech.RootTower.exponentRemainder_split line 33
  7. lemma OAI.Lech.RootTower.exponentQuotient_split line 39
  8. lemma OAI.Lech.RootTower.coeff_expansion_monomial_eq_zero line 45
  9. lemma OAI.Lech.RootTower.coeff_expansion_monomial_split line 61
  10. def OAI.Lech.RootTower.extract line 68
  11. lemma OAI.Lech.RootTower.sum_expansion_extract line 71
  12. lemma OAI.Lech.RootTower.coeff_sum_expansion line 85
  13. def OAI.Lech.RootTower.Expanded line 99
  14. instance OAI.Lech.RootTower.expandedCommRing line 101
  15. instance OAI.Lech.RootTower.expandedAlgebra line 104
  16. def OAI.Lech.RootTower.expansionMap line 108
  17. lemma OAI.Lech.RootTower.expansionMap_bijective line 122
  18. def OAI.Lech.RootTower.expansionEquiv line 133
  19. def OAI.Lech.RootTower.expansionBasis line 138
  20. lemma OAI.Lech.RootTower.expanded_free line 142
  21. lemma OAI.Lech.RootTower.expansion_flat line 145
  22. lemma OAI.Lech.RootTower.expansion_local line 150
  23. lemma OAI.Lech.RootTower.map_bijective_of_bijective line 158
  24. instance OAI.Lech.RootTower.powerSeriesCharP line 172
  25. lemma OAI.Lech.RootTower.iterateFrobenius_flat line 176
  26. lemma OAI.Lech.RootTower.fiber_length_of_basis line 198
  27. lemma OAI.Lech.RootTower.residue_eq_constant line 225
  28. def OAI.Lech.RootTower.FrobeniusExpanded line 235
  29. instance OAI.Lech.RootTower.frobeniusExpandedRing line 236
  30. instance OAI.Lech.RootTower.frobeniusExpandedLocal line 238
  31. instance OAI.Lech.RootTower.frobeniusExpandedAlgebra line 240
  32. def OAI.Lech.RootTower.expansionToFrobeniusMap line 244
  33. def OAI.Lech.RootTower.expansionToFrobenius line 256
  34. def OAI.Lech.RootTower.frobeniusBasis line 262
  35. instance OAI.Lech.RootTower.frobeniusExpandedLocalHom line 267
  36. lemma OAI.Lech.RootTower.frobenius_residue_surjective line 275
  37. lemma OAI.Lech.RootTower.frobenius_fiber_length line 287
  38. def OAI.Lech.RootTower.rootMap line 305
  39. lemma OAI.Lech.RootTower.rootMap_injective line 318
  40. lemma OAI.Lech.RootTower.rootMap_transition line 322
  41. def OAI.Lech.RootTower.rootRing line 328
  42. lemma OAI.Lech.RootTower.rootRing_mono line 330
  43. def OAI.Lech.RootTower.rootEquiv line 335
  44. lemma OAI.Lech.RootTower.rootEquiv_apply line 340
  45. lemma OAI.Lech.RootTower.rootRing_exhaustive line 343
  46. instance OAI.Lech.RootTower.rootRing_local line 347
  47. instance OAI.Lech.RootTower.rootRing_noetherian line 350
  48. lemma OAI.Lech.RootTower.root_inclusion_eq line 354
  49. lemma OAI.Lech.RootTower.root_inclusion_flat line 364
  50. lemma OAI.Lech.RootTower.iterateFrobenius_local line 371
  51. lemma OAI.Lech.RootTower.root_inclusion_local line 376
  52. lemma OAI.Lech.RootTower.self_length_ringEquiv line 391
  53. lemma OAI.Lech.RootTower.quotient_length_ringEquiv line 400
  54. lemma OAI.Lech.RootTower.root_inclusion_comp_equiv line 414
  55. lemma OAI.Lech.RootTower.root_fiber_ideal line 421
  56. lemma OAI.Lech.RootTower.root_fiber_length line 438