OAI/AlgebraicGeometry/Seshadri/Blowup/ReesAlgebra.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.ReesGrading.piece line 15
  2. lemma OAI.MaximalSeshadri.ReesGrading.mem_piece line 25
  3. def OAI.MaximalSeshadri.ReesGrading.component line 28
  4. lemma OAI.MaximalSeshadri.ReesGrading.component_val line 32
  5. def OAI.MaximalSeshadri.ReesGrading.components line 35
  6. lemma OAI.MaximalSeshadri.ReesGrading.components_apply line 47
  7. def OAI.MaximalSeshadri.ReesGrading.componentsAdd line 50
  8. lemma OAI.MaximalSeshadri.ReesGrading.piece_coeff_ne line 61
  9. lemma OAI.MaximalSeshadri.ReesGrading.components_of_piece line 65
  10. lemma OAI.MaximalSeshadri.ReesGrading.recompose_components line 79
  11. instance OAI.MaximalSeshadri.ReesGrading.gradedMonoid line 106
  12. instance OAI.MaximalSeshadri.ReesGrading.grading line 113
  13. def OAI.MaximalSeshadri.ReesGrading.affineBlowup line 126
  14. def OAI.MaximalSeshadri.ReesGrading.zeroEquiv line 128
  15. def OAI.MaximalSeshadri.ReesGrading.zeroIso line 142
  16. def OAI.MaximalSeshadri.ReesGrading.projection line 145
  17. instance OAI.MaximalSeshadri.ReesGrading.(instance at line 148) line 148
  18. instance OAI.MaximalSeshadri.ReesGrading.(instance at line 152) line 152
  19. instance OAI.MaximalSeshadri.ReesGrading.projection_proper line 155
  20. def OAI.MaximalSeshadri.ReesGrading.generator line 168
  21. lemma OAI.MaximalSeshadri.ReesGrading.generator_val line 171
  22. lemma OAI.MaximalSeshadri.ReesGrading.generator_mem line 174
  23. def OAI.MaximalSeshadri.ReesGrading.evaluation line 177
  24. lemma OAI.MaximalSeshadri.ReesGrading.evaluation_generator line 180
  25. lemma OAI.MaximalSeshadri.ReesGrading.evaluation_piece line 183
  26. abbrev OAI.MaximalSeshadri.ReesGrading.chart line 189
  27. def OAI.MaximalSeshadri.ReesGrading.chartMap line 191
  28. lemma OAI.MaximalSeshadri.ReesGrading.chartMap_mk line 198
  29. lemma OAI.MaximalSeshadri.ReesGrading.chartMap_injective line 209
  30. def OAI.MaximalSeshadri.ReesGrading.chartBase line 233
  31. lemma OAI.MaximalSeshadri.ReesGrading.chartMap_base line 237
  32. def OAI.MaximalSeshadri.ReesGrading.ratio line 250
  33. lemma OAI.MaximalSeshadri.ReesGrading.chartMap_ratio line 254
  34. lemma OAI.MaximalSeshadri.ReesGrading.base_mul_ratio line 260
  35. lemma OAI.MaximalSeshadri.ReesGrading.map_ideal_principal line 267
  36. lemma OAI.MaximalSeshadri.ReesGrading.chart_isDomain line 278
  37. lemma OAI.MaximalSeshadri.ReesGrading.chartBase_injective line 282
  38. lemma OAI.MaximalSeshadri.ReesGrading.chart_generator_regular line 289