OAI/NumberTheory/PiExponent/Jets/CompactLogJetIdeal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.CompactLogJetIdeal.coordinateRing line 15
  2. abbrev OAI.PiExponent.CompactLogJetIdeal.affineSpace line 16
  3. abbrev OAI.PiExponent.CompactLogJetIdeal.base line 17
  4. def OAI.PiExponent.CompactLogJetIdeal.structureMap line 19
  5. def OAI.PiExponent.CompactLogJetIdeal.point line 22
  6. theorem OAI.PiExponent.CompactLogJetIdeal.point_section line 25
  7. theorem OAI.PiExponent.CompactLogJetIdeal.range_point line 35
  8. theorem OAI.PiExponent.CompactLogJetIdeal.support_specIdeal line 42
  9. def OAI.PiExponent.CompactLogJetIdeal.polynomialIdeal line 50
  10. def OAI.PiExponent.CompactLogJetIdeal.affineIdeal line 54
  11. theorem OAI.PiExponent.CompactLogJetIdeal.support_affineIdeal line 58
  12. def OAI.PiExponent.CompactLogJetIdeal.compactIdeal line 74
  13. theorem OAI.PiExponent.CompactLogJetIdeal.restrict_compactIdeal line 79
  14. theorem OAI.PiExponent.CompactLogJetIdeal.support_compactIdeal line 85
  15. theorem OAI.PiExponent.CompactLogJetIdeal.compactIdeal_isFinitePresentation line 99
  16. theorem OAI.PiExponent.CompactLogJetIdeal.polynomialIdeal_pow_le line 105
  17. theorem OAI.PiExponent.CompactLogJetIdeal.formalJet_packet_zero_of_mem_polynomialIdeal_pow line 112