OAI/RingTheory/Multiplicity/ExceptionalFibre.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Lech.ReesRoot.coefficientAlgebra line 32
  2. instance OAI.Lech.ReesRoot.coefficientTower line 37
  3. def OAI.Lech.ReesRoot.exceptionalProjectiveMap line 41
  4. instance OAI.Lech.ReesRoot.exceptionalAlgebra line 44
  5. instance OAI.Lech.ReesRoot.exceptionalTower line 54
  6. def OAI.Lech.ReesRoot.coefficientReductionLinear line 60
  7. def OAI.Lech.ReesRoot.reductionLinear line 64
  8. def OAI.Lech.ReesRoot.coefficientComparisonLinear line 73
  9. lemma OAI.Lech.ReesRoot.coefficientReductionLinear_surjective line 83
  10. lemma OAI.Lech.ReesRoot.reductionLinear_surjective line 85
  11. lemma OAI.Lech.ReesRoot.coefficientComparisonLinear_surjective line 87
  12. lemma OAI.Lech.ReesRoot.coefficientReductionLinear_kernel line 90
  13. lemma OAI.Lech.ReesRoot.reductionLinear_kernel line 96
  14. lemma OAI.Lech.ReesRoot.coefficient_torsion line 100
  15. abbrev OAI.Lech.ReesRoot.RootFibreSections line 116
  16. def OAI.Lech.ReesRoot.rootFibreMap line 121
  17. lemma OAI.Lech.ReesRoot.fibre_unit_square line 126
  18. lemma OAI.Lech.ReesRoot.rootFibreMap_surjective line 134
  19. lemma OAI.Lech.ReesRoot.coefficientComparisonLinear_kernel_zero line 142
  20. lemma OAI.Lech.ReesRoot.rootFibreMap_kernel_zero line 153