OAI/RingTheory/Multiplicity/IdealGradedRing.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.IdealGraded.Ring line 16
  2. lemma OAI.Lech.IdealGraded.scalar_mem_shifted line 18
  3. instance OAI.Lech.IdealGraded.gradedAlgebra line 26
  4. instance OAI.Lech.IdealGraded.gradedTower line 29
  5. abbrev OAI.Lech.IdealGraded.quotientR line 32
  6. lemma OAI.Lech.IdealGraded.quotientR_ker_homogeneous line 34
  7. instance OAI.Lech.IdealGraded.imageGrading line 38
  8. def OAI.Lech.IdealGraded.grade line 42
  9. instance OAI.Lech.IdealGraded.gradeDecomposition line 49
  10. lemma OAI.Lech.IdealGraded.monomial_mem_shifted_iff line 54
  11. def OAI.Lech.IdealGraded.toRingR line 66
  12. lemma OAI.Lech.IdealGraded.toRingR_injective line 72
  13. lemma OAI.Lech.IdealGraded.toRingR_mem line 79
  14. def OAI.Lech.IdealGraded.toPiece line 83
  15. lemma OAI.Lech.IdealGraded.toPiece_bijective line 92
  16. def OAI.Lech.IdealGraded.pieceEquiv line 100
  17. instance OAI.Lech.IdealGraded.gradeFinite line 103
  18. lemma OAI.Lech.IdealGraded.grade_mul line 106
  19. lemma OAI.Lech.IdealGraded.exists_generators line 121
  20. lemma OAI.Lech.Grading.aeval_mem line 163
  21. def OAI.Lech.Grading.polynomialMap line 184
  22. lemma OAI.Lech.Grading.polynomialMap_surjective line 188
  23. instance OAI.Lech.IdealGraded.gradeGradedAlgebra line 199
  24. def OAI.Lech.IdealGraded.generator line 207
  25. lemma OAI.Lech.IdealGraded.generator_mem line 210
  26. lemma OAI.Lech.IdealGraded.generator_adjoin line 213
  27. def OAI.Lech.IdealGraded.polynomialMap line 237
  28. lemma OAI.Lech.IdealGraded.polynomialMap_surjective line 240
  29. instance OAI.Lech.Homogeneous.module line 256
  30. def OAI.Lech.Homogeneous.fraction line 261
  31. def OAI.Lech.Homogeneous.gradedMap line 275
  32. def OAI.Lech.Homogeneous.awayMap line 280
  33. lemma OAI.Lech.Homogeneous.awayMap_fraction line 293
  34. lemma OAI.Lech.Homogeneous.gradedMap_surjective line 299
  35. lemma OAI.Lech.Homogeneous.awayMap_surjective line 309
  36. lemma OAI.Lech.Homogeneous.kernel_fraction line 320
  37. def OAI.Lech.Homogeneous.kernelFraction line 368
  38. lemma OAI.Lech.Homogeneous.iSup_range_kernelFraction line 378
  39. theorem OAI.Lech.Homogeneous.kernel_property line 389
  40. def OAI.Lech.Grading.MonomialIndex line 415
  41. def OAI.Lech.Grading.indexEquiv line 416
  42. instance OAI.Lech.Grading.indexFintype line 418
  43. lemma OAI.Lech.Grading.index_card line 420
  44. def OAI.Lech.Grading.homogeneousEquiv line 423