OAI/RingTheory/Multiplicity/LechLevel.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.IdealFiltration.level line 15
  2. def OAI.Lech.IdealFiltration.next line 17
  3. abbrev OAI.Lech.IdealFiltration.Piece line 20
  4. lemma OAI.Lech.IdealFiltration.level_succ_le line 22
  5. def OAI.Lech.IdealFiltration.inclusion line 25
  6. lemma OAI.Lech.IdealFiltration.inclusion_injective line 31
  7. def OAI.Lech.IdealFiltration.transition line 36
  8. lemma OAI.Lech.IdealFiltration.transition_surjective line 40
  9. lemma OAI.Lech.IdealFiltration.piece_exact line 46
  10. lemma OAI.Lech.IdealFiltration.quotient_torsion line 52
  11. lemma OAI.Lech.IdealFiltration.piece_torsion line 58
  12. lemma OAI.Lech.IdealFiltration.length_successor line 64
  13. lemma OAI.Lech.IdealFiltration.length_eq_sum line 72
  14. lemma OAI.Lech.IdealFiltration.length_quotient line 84
  15. lemma OAI.Lech.powerTorsion_quotient line 100
  16. lemma OAI.Lech.powerTorsion_pi_small line 104
  17. lemma OAI.Lech.TorsionLength.value_fintype_small line 117
  18. def OAI.Lech.ResidueGenerators.coefficient line 130
  19. lemma OAI.Lech.ResidueGenerators.coefficient_mk line 135
  20. def OAI.Lech.ResidueGenerators.map line 139
  21. lemma OAI.Lech.ResidueGenerators.generators_mem_range line 143
  22. lemma OAI.Lech.ResidueGenerators.surjective_of_span line 151
  23. lemma OAI.Lech.ResidueGenerators.value_le line 160
  24. lemma OAI.Lech.span_subquotient line 177
  25. def OAI.Lech.MonomialSpanning.monic line 195
  26. lemma OAI.Lech.MonomialSpanning.span_monic_degree line 198
  27. lemma OAI.Lech.MonomialSpanning.monic_mem_power line 211
  28. lemma OAI.Lech.MonomialSpanning.monic_mem_powers line 216
  29. def OAI.Lech.MonomialSpanning.Bounded line 225
  30. instance OAI.Lech.MonomialSpanning.boundedFintype line 227
  31. def OAI.Lech.MonomialSpanning.exponent line 232
  32. lemma OAI.Lech.MonomialSpanning.exponent_apply line 235
  33. lemma OAI.Lech.MonomialSpanning.exponent_degree line 238
  34. lemma OAI.Lech.MonomialSpanning.exists_bounded line 242
  35. lemma OAI.Lech.MonomialSpanning.power_le_bounded_span line 249
  36. lemma OAI.Lech.IdealFiltration.piece_annihilator line 267
  37. def OAI.Lech.MonomialSpanning.lift line 284
  38. def OAI.Lech.MonomialSpanning.pieceGenerator line 290
  39. lemma OAI.Lech.MonomialSpanning.pieceGenerator_span line 295
  40. lemma OAI.Lech.MonomialSpanning.piece_value_le line 304
  41. lemma OAI.Lech.MonomialSpanning.bounded_degree_le line 316
  42. def OAI.Lech.MonomialSpanning.boundedSigmaEquiv line 323
  43. lemma OAI.Lech.MonomialSpanning.sum_bounded_card line 334
  44. lemma OAI.Lech.MonomialSpanning.powers_contain_power line 341
  45. lemma OAI.Lech.ennreal_finite_sum_saturated line 357
  46. lemma OAI.Lech.TorsionLength.kernel_zero_of_surjective_value_eq line 372
  47. lemma OAI.Lech.MonomialSpanning.piece_value_eq line 389
  48. lemma OAI.Lech.MonomialSpanning.piece_map_kernel_zero line 412