OAI/RingTheory/Multiplicity/IdealGradedLengthPiece.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.IdealGraded.length_piece_eq_length line 32
  2. lemma OAI.Lech.IdealGraded.eventuallyPolynomial_piece_length line 38
  3. lemma OAI.Lech.IdealGraded.eventuallyPolynomial_length_of_artinian line 50
  4. lemma OAI.Lech.Primary.artinian_quotient line 76
  5. lemma OAI.Lech.Primary.exists_maximal_pow_le line 82
  6. def OAI.Lech.Primary.colength line 86
  7. lemma OAI.Lech.Primary.length_ne_top line 89
  8. lemma OAI.Lech.Primary.colength_cast line 98
  9. lemma OAI.Lech.Primary.colength_mono line 102
  10. lemma OAI.Lech.Primary.polynomial_bound line 109
  11. def OAI.Lech.Primary.normalizedColength line 122
  12. def OAI.Lech.Primary.multiplicity line 125
  13. theorem OAI.Lech.Primary.multiplicity_is_limit line 128
  14. lemma OAI.Lech.Primary.multiplicity_nonneg line 144
  15. lemma OAI.Lech.Primary.multiplicity_antitone line 151
  16. lemma OAI.Lech.Primary.maximal_multiplicity_eq line 161
  17. lemma OAI.Lech.FrobeniusGrowth.powerIdeal_le_pow line 172
  18. lemma OAI.Lech.FrobeniusGrowth.ordinary_error_tendsto line 177
  19. lemma OAI.Lech.FrobeniusGrowth.normalized_error_of_linear_containment line 200
  20. lemma OAI.Lech.FrobeniusGrowth.parameter_power_linear_containment line 229
  21. lemma OAI.Lech.FrobeniusGrowth.parameter_error_tendsto line 239
  22. def OAI.Lech.ordinaryLength line 268
  23. instance OAI.Lech.RootTower.expandedLocal line 284
  24. instance OAI.Lech.RootTower.expandedLocalHom line 286
  25. lemma OAI.Lech.RootTower.expansion_residue_surjective line 291
  26. lemma OAI.Lech.RootTower.variable_powers_colength line 301
  27. lemma OAI.Lech.PowerSeries.maximal_power_colength line 328
  28. lemma OAI.Lech.ascFactorial_normalized_tendsto line 366
  29. lemma OAI.Lech.binomial_normalized_tendsto line 385