OAI/NumberTheory/PiExponent/LocalAlgebra/WeightedBezout.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.WeightedBezout.translatedPowerSubstitution line 16
  2. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_X line 20
  3. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_C line 25
  4. theorem OAI.PiExponent.WeightedBezout.totalDegree_aeval_monomial_le line 29
  5. theorem OAI.PiExponent.WeightedBezout.totalDegree_aeval_le_weighted line 45
  6. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_totalDegree line 56
  7. def OAI.PiExponent.WeightedBezout.translation line 63
  8. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_factor line 66
  9. def OAI.PiExponent.WeightedBezout.translationEquiv line 72
  10. def OAI.PiExponent.WeightedBezout.pointIdeal line 77
  11. instance OAI.PiExponent.WeightedBezout.pointIdeal_isMaximal line 80
  12. theorem OAI.PiExponent.WeightedBezout.mem_pointIdeal line 85
  13. theorem OAI.PiExponent.WeightedBezout.pointIdeal_eq_span line 88
  14. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_eval_origin line 116
  15. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_comap_origin line 123
  16. theorem OAI.PiExponent.WeightedBezout.prime_over_pointIdeal_eq_origin line 136
  17. theorem OAI.PiExponent.WeightedBezout.pointIdeal_map_translatedPowerSubstitution line 156
  18. theorem OAI.PiExponent.WeightedBezout.translatedPowerSubstitution_totalDegree_real line 165
  19. theorem OAI.PiExponent.WeightedBezout.origin_minimalPrimes_map line 187