OAI/RingTheory/Multiplicity/ReesExceptionalRing.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.Homogeneous.zeroPieceEquiv_val line 18
  2. lemma OAI.Lech.Homogeneous.zeroPieceEquiv_symm_val line 20
  3. lemma OAI.Lech.Homogeneous.zeroPiece_natural line 25
  4. abbrev OAI.Lech.FilteredFraction.ReesChart line 48
  5. abbrev OAI.Lech.FilteredFraction.ExceptionalChart line 49
  6. def OAI.Lech.FilteredFraction.chartEquiv line 56
  7. def OAI.Lech.FilteredFraction.exceptionalChartEquiv line 59
  8. lemma OAI.Lech.FilteredFraction.exceptionalChartEquiv_symm_val line 63
  9. def OAI.Lech.FilteredFraction.chartReduction line 68
  10. lemma OAI.Lech.FilteredFraction.chartReduction_surjective line 73
  11. lemma OAI.Lech.FilteredFraction.chartReduction_layerMap line 77
  12. def OAI.Lech.FilteredFraction.chartAmbient line 87
  13. lemma OAI.Lech.FilteredFraction.chartReduction_val line 92
  14. lemma OAI.Lech.FilteredFraction.chartReduction_mk line 101
  15. def OAI.Lech.FilteredFraction.chartReductionAlg line 121
  16. lemma OAI.Lech.FilteredFraction.chartReduction_eq_zero_iff line 137
  17. lemma OAI.Lech.FilteredFraction.scalar_mem_next line 146
  18. lemma OAI.Lech.FilteredFraction.chartReduction_kernel line 161
  19. def OAI.Lech.FilteredFraction.exceptionalQuotientEquiv line 187