OAI/NumberTheory/SiegelZeros/Intersection/TorusPolynomial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.W17.coordinateProduct_ne_zero line 18
  2. theorem OAI.SiegelZeros.W17.polynomial_to_torus_injective line 22
  3. theorem OAI.SiegelZeros.W17.polynomial_to_torus_ne_zero line 27
  4. theorem OAI.SiegelZeros.W17.torus_isDomain line 34
  5. def OAI.SiegelZeros.W17.torusZeroIdeal line 38
  6. abbrev OAI.SiegelZeros.W17.TorusHypersurfaceRing line 41
  7. theorem OAI.SiegelZeros.W17.torusZeroIdeal_ne_bot line 44
  8. theorem OAI.SiegelZeros.W17.torusZeroIdeal_le_identity line 53
  9. theorem OAI.SiegelZeros.W17.torusZeroIdeal_ne_top line 60
  10. def OAI.SiegelZeros.W17.torusZeroLocus line 68
  11. theorem OAI.SiegelZeros.W17.torusZeroLocus_isClosed line 71
  12. theorem OAI.SiegelZeros.W17.torusZeroLocus_nonempty line 74
  13. theorem OAI.SiegelZeros.W17.torusZeroLocus_ne_univ line 84
  14. theorem OAI.SiegelZeros.W17.iterate_invariantDerivation_mem line 97
  15. def OAI.SiegelZeros.W17.derivativeJet line 107
  16. theorem OAI.SiegelZeros.W17.derivativeJet_mem line 113
  17. theorem OAI.SiegelZeros.W17.derivativeJet_totalDegree_lt line 120