OAI/RingTheory/Multiplicity/PrimeFiltrationSupport.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.ArtinReesLength.induced line 10
  2. lemma OAI.Lech.ArtinReesLength.internal_le_induced line 11
  3. lemma OAI.Lech.ArtinReesLength.exists_shift line 13
  4. lemma OAI.Lech.ArtinReesLength.length_exact line 23
  5. lemma OAI.Lech.ArtinReesLength.quotient_length_antitone line 50
  6. lemma OAI.Lech.ArtinReesLength.length_upper line 54
  7. lemma OAI.Lech.ArtinReesLength.exists_length_lower line 61
  8. lemma OAI.Lech.ArtinReesLength.finite_quotient_length line 75
  9. def OAI.Lech.ArtinReesLength.colength line 92
  10. lemma OAI.Lech.ArtinReesLength.colength_cast line 95
  11. lemma OAI.Lech.ArtinReesLength.shifted_denominator line 102
  12. theorem OAI.Lech.ArtinReesLength.normalized_additivity line 120
  13. inductive OAI.Lech.PrimeFiltration.Above line 154
  14. lemma OAI.Lech.PrimeFiltration.next line 159
  15. theorem OAI.Lech.PrimeFiltration.exists_above line 198
  16. lemma OAI.Lech.ArtinReesLength.colength_equiv line 211
  17. lemma OAI.Lech.ArtinReesLength.cyclic_colength line 227
  18. lemma OAI.Lech.PrimeFiltration.primary_quotient line 245
  19. lemma OAI.Lech.PrimeFiltration.quotient_dimension_le line 256
  20. lemma OAI.Lech.PrimeFiltration.primary_unscaled_limit line 263
  21. lemma OAI.Lech.PrimeFiltration.lower_dimension_limit line 274
  22. def OAI.Lech.PrimeFiltration.contribution line 284
  23. lemma OAI.Lech.PrimeFiltration.cyclic_limit line 293
  24. theorem OAI.Lech.PrimeFiltration.limit_of_above line 311
  25. theorem OAI.Lech.PrimeFiltration.exists_limit_decomposition line 343
  26. lemma OAI.Lech.LocalizationLength.tensor_length_exact line 356
  27. lemma OAI.Lech.LocalizationLength.tensor_cyclic_length line 365
  28. lemma OAI.Lech.LocalizationLength.local_cyclic_self line 371
  29. lemma OAI.Lech.LocalizationLength.local_cyclic_zero line 380
  30. lemma OAI.Lech.PrimeFiltration.eq_of_le_full_dim line 399
  31. lemma OAI.Lech.PrimeFiltration.full_dim_minimal line 413
  32. inductive OAI.Lech.PrimeFiltration.Factors line 423
  33. lemma OAI.Lech.PrimeFiltration.factors_of_above line 429
  34. lemma OAI.Lech.PrimeFiltration.Factors.isPrime line 436
  35. lemma OAI.Lech.PrimeFiltration.Factors.tensor_length line 447
  36. lemma OAI.Lech.PrimeFiltration.Factors.localized_length line 460
  37. lemma OAI.Lech.PrimeFiltration.Factors.colength_limit line 490