OAI/NumberTheory/PiExponent/Ampleness/ReesPushdown.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.ReesGrading.piece line 14
  2. lemma OAI.PiExponentSeshadri.ReesGrading.mem_piece line 24
  3. def OAI.PiExponentSeshadri.ReesGrading.component line 27
  4. lemma OAI.PiExponentSeshadri.ReesGrading.component_val line 31
  5. def OAI.PiExponentSeshadri.ReesGrading.components line 34
  6. lemma OAI.PiExponentSeshadri.ReesGrading.components_apply line 46
  7. def OAI.PiExponentSeshadri.ReesGrading.componentsAdd line 49
  8. lemma OAI.PiExponentSeshadri.ReesGrading.piece_coeff_ne line 60
  9. lemma OAI.PiExponentSeshadri.ReesGrading.components_of_piece line 64
  10. lemma OAI.PiExponentSeshadri.ReesGrading.recompose_components line 78
  11. instance OAI.PiExponentSeshadri.ReesGrading.gradedMonoid line 105
  12. instance OAI.PiExponentSeshadri.ReesGrading.grading line 112
  13. def OAI.PiExponentSeshadri.ReesGrading.affineBlowup line 125
  14. def OAI.PiExponentSeshadri.ReesGrading.zeroEquiv line 127
  15. def OAI.PiExponentSeshadri.ReesGrading.zeroIso line 141
  16. def OAI.PiExponentSeshadri.ReesGrading.projection line 144
  17. instance OAI.PiExponentSeshadri.ReesGrading.(instance at line 147) line 147
  18. instance OAI.PiExponentSeshadri.ReesGrading.(instance at line 151) line 151
  19. instance OAI.PiExponentSeshadri.ReesGrading.projection_proper line 154
  20. def OAI.PiExponentSeshadri.ReesGrading.generator line 166
  21. lemma OAI.PiExponentSeshadri.ReesGrading.generator_val line 169
  22. lemma OAI.PiExponentSeshadri.ReesGrading.generator_mem line 172
  23. def OAI.PiExponentSeshadri.ReesGrading.evaluation line 175
  24. lemma OAI.PiExponentSeshadri.ReesGrading.evaluation_generator line 178
  25. lemma OAI.PiExponentSeshadri.ReesGrading.evaluation_piece line 181
  26. abbrev OAI.PiExponentSeshadri.ReesGrading.chart line 187
  27. def OAI.PiExponentSeshadri.ReesGrading.chartMap line 189
  28. lemma OAI.PiExponentSeshadri.ReesGrading.chartMap_mk line 196
  29. lemma OAI.PiExponentSeshadri.ReesGrading.chartMap_injective line 207
  30. def OAI.PiExponentSeshadri.ReesGrading.chartBase line 231
  31. lemma OAI.PiExponentSeshadri.ReesGrading.chartMap_base line 235
  32. def OAI.PiExponentSeshadri.ReesGrading.ratio line 248
  33. lemma OAI.PiExponentSeshadri.ReesGrading.chartMap_ratio line 252
  34. lemma OAI.PiExponentSeshadri.ReesGrading.base_mul_ratio line 258
  35. lemma OAI.PiExponentSeshadri.ReesGrading.map_ideal_principal line 265
  36. lemma OAI.PiExponentSeshadri.ReesGrading.chart_isDomain line 276
  37. lemma OAI.PiExponentSeshadri.ReesGrading.chartBase_injective line 280
  38. lemma OAI.PiExponentSeshadri.ReesGrading.chart_generator_regular line 287
  39. def OAI.PiExponent.ReesPushdown.ordinaryPowerEquivPiece line 311
  40. theorem OAI.PiExponent.ReesPushdown.coeff_mem_ordinaryPower line 327
  41. theorem OAI.PiExponent.ReesPushdown.chart_ordinaryPower_principal line 330
  42. theorem OAI.PiExponent.ReesPushdown.ordinaryPowerEquivPiece_apply_coeff line 334
  43. theorem OAI.PiExponent.ReesPushdown.chart_ordinaryPower_fraction line 338
  44. theorem OAI.PiExponent.ReesPushdown.eventually_no_power_torsion line 361
  45. theorem OAI.PiExponent.ReesPushdown.exists_power_annihilating_of_chart_vanish line 392
  46. theorem OAI.PiExponent.ReesPushdown.eventually_chart_family_injective_on_ordinaryPowers line 418
  47. theorem OAI.PiExponent.ReesPushdown.eventually_chart_family_injective line 426