OAI/NumberTheory/PiExponent/Jets/JetGeometry.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.JetGeometry.weightedIdeal line 14
  2. theorem OAI.PiExponent.JetGeometry.mem_weightedIdeal line 22
  3. theorem OAI.PiExponent.JetGeometry.mem_weightedIdeal_iff line 26
  4. theorem OAI.PiExponent.JetGeometry.weightedIdeal_mul_le line 36
  5. theorem OAI.PiExponent.JetGeometry.ideal_pow_le_weightedIdeal line 45
  6. def OAI.PiExponent.JetGeometry.coordinatePowerIdeal line 59
  7. theorem OAI.PiExponent.JetGeometry.X_pow_mem_weightedIdeal line 62
  8. theorem OAI.PiExponent.JetGeometry.coordinatePowerIdeal_pow_le line 77
  9. theorem OAI.PiExponent.JetGeometry.quotient_surjective_of_le line 86
  10. def OAI.PiExponent.JetGeometry.CoefficientPacket line 97
  11. def OAI.PiExponent.JetGeometry.coefficientPacket line 100
  12. theorem OAI.PiExponent.JetGeometry.coefficientPacket_surjective_of_quotient line 103
  13. theorem OAI.PiExponent.JetGeometry.coefficientPacket_surjective_of_coordinatePowerIdeal line 124
  14. theorem OAI.PiExponent.JetGeometry.rational_weight_nonneg line 133
  15. def OAI.PiExponent.JetGeometry.rationalWeightedIdeal line 138
  16. theorem OAI.PiExponent.JetGeometry.mem_rationalWeightedIdeal line 158
  17. theorem OAI.PiExponent.JetGeometry.rationalWeightedIdeal_mul_le line 163
  18. theorem OAI.PiExponent.JetGeometry.ideal_pow_le_rationalWeightedIdeal line 183
  19. theorem OAI.PiExponent.JetGeometry.coordinatePowerIdeal_pow_le_rational line 200
  20. def OAI.PiExponent.JetGeometry.RationalCoefficientPacket line 215
  21. def OAI.PiExponent.JetGeometry.rationalCoefficientPacket line 218
  22. theorem OAI.PiExponent.JetGeometry.rationalCoefficientPacket_surjective_of_coordinatePowerIdeal line 221
  23. theorem OAI.PiExponent.JetGeometry.rationalCoefficientPackets_surjective_of_coordinatePowerIdeal line 244