OAI/NumberTheory/PiExponent/Polynomials/WeightedMonomialImage.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.WeightedCompactification.monomialImage line 16
  2. abbrev OAI.PiExponent.WeightedCompactification.ambientGrade line 18
  3. def OAI.PiExponent.WeightedCompactification.gradedMonomialMapInt line 21
  4. theorem OAI.PiExponent.WeightedCompactification.monomialImage_homogeneous line 26
  5. abbrev OAI.PiExponent.WeightedCompactification.imageGrade line 34
  6. instance OAI.PiExponent.WeightedCompactification.imageGradedAlgebra line 36
  7. def OAI.PiExponent.WeightedCompactification.gradedImageMap line 39
  8. theorem OAI.PiExponent.WeightedCompactification.gradedImageMap_surjective line 44
  9. def OAI.PiExponent.WeightedCompactification.monomialQuotientEquivImage line 48
  10. instance OAI.PiExponent.WeightedCompactification.monomialHomogeneousIdeal_isPrime line 52
  11. abbrev OAI.PiExponent.WeightedCompactification.imageCoordinate line 56
  12. theorem OAI.PiExponent.WeightedCompactification.imageCoordinate_mem line 59
  13. def OAI.PiExponent.WeightedCompactification.imageEvaluation line 63
  14. theorem OAI.PiExponent.WeightedCompactification.imageEvaluation_coordinate line 67
  15. theorem OAI.PiExponent.WeightedCompactification.unit_homogeneous_formula line 71
  16. theorem OAI.PiExponent.WeightedCompactification.imageEvaluation_homogeneous_eq_zero line 89