OAI/RingTheory/Multiplicity/LechBoundedEquiv.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.MonomialSpanning.boundedEquivTotal line 16
  2. lemma OAI.Lech.MonomialSpanning.bounded_card_of_lt line 26
  3. lemma OAI.Lech.MonomialSpanning.powers_le_power line 33
  4. lemma OAI.Lech.MonomialSpanning.piece_value_eq_of_levels line 40
  5. lemma OAI.Lech.MonomialSpanning.ordinary_piece_value line 56
  6. lemma OAI.Lech.MonomialSpanning.power_colength line 71
  7. def OAI.Lech.Grading.imagePiece line 103
  8. def OAI.Lech.Grading.pieceMap line 105
  9. lemma OAI.Lech.Grading.pieceMap_coe line 109
  10. def OAI.Lech.Grading.beforeQuotient line 112
  11. lemma OAI.Lech.Grading.beforeQuotient_piece line 115
  12. lemma OAI.Lech.Grading.kernel_le_beforeQuotient line 119
  13. def OAI.Lech.Grading.imageDecompose line 128
  14. lemma OAI.Lech.Grading.imageDecompose_map line 133
  15. lemma OAI.Lech.Grading.recompose_beforeQuotient line 139
  16. def OAI.Lech.Grading.imageDecomposition line 147
  17. def OAI.Lech.Grading.subPiece line 169
  18. def OAI.Lech.Grading.subPieceMap line 171
  19. def OAI.Lech.Grading.subDecompose line 176
  20. lemma OAI.Lech.Grading.subDecompose_lmap line 201
  21. lemma OAI.Lech.Grading.sub_lmap_recompose line 208
  22. def OAI.Lech.Grading.subDecomposition line 219
  23. def OAI.Lech.IdealGraded.nextPower line 256
  24. abbrev OAI.Lech.IdealGraded.Piece line 259
  25. lemma OAI.Lech.IdealGraded.pow_succ_le line 261
  26. lemma OAI.Lech.IdealGraded.torsion_piece line 264
  27. instance OAI.Lech.IdealGraded.pieceModule line 272
  28. instance OAI.Lech.IdealGraded.pieceTower line 275
  29. def OAI.Lech.IdealGraded.inclusion line 279
  30. lemma OAI.Lech.IdealGraded.inclusion_injective line 285
  31. def OAI.Lech.IdealGraded.transition line 290
  32. lemma OAI.Lech.IdealGraded.transition_surjective line 294
  33. lemma OAI.Lech.IdealGraded.piece_exact line 300
  34. lemma OAI.Lech.IdealGraded.length_successor line 306
  35. lemma OAI.Lech.IdealGraded.length_eq_sum line 312
  36. instance OAI.Lech.IdealGraded.pieceFinite line 319
  37. lemma OAI.Lech.IdealGraded.length_piece_eq_finrank line 323
  38. def OAI.Lech.IdealGraded.monomial line 339
  39. lemma OAI.Lech.IdealGraded.monomial_coe line 343
  40. def OAI.Lech.IdealGraded.coefficient line 346
  41. lemma OAI.Lech.IdealGraded.coefficient_coe line 350
  42. lemma OAI.Lech.IdealGraded.coefficient_monomial line 353
  43. lemma OAI.Lech.IdealGraded.monomial_injective line 359
  44. abbrev OAI.Lech.IdealGraded.reesGrade line 362
  45. def OAI.Lech.IdealGraded.component line 364
  46. lemma OAI.Lech.IdealGraded.component_coe line 367
  47. def OAI.Lech.IdealGraded.reesDecompose line 370
  48. lemma OAI.Lech.IdealGraded.reesDecompose_apply line 385
  49. lemma OAI.Lech.IdealGraded.reesDecompose_support line 388
  50. lemma OAI.Lech.IdealGraded.reesDecompose_monomial line 398
  51. instance OAI.Lech.IdealGraded.reesDecomposition line 412
  52. lemma OAI.Lech.IdealGraded.rees_decompose_val line 438
  53. def OAI.Lech.IdealGraded.shifted line 443
  54. lemma OAI.Lech.IdealGraded.shifted_homogeneous line 457