OAI/NumberTheory/PiExponent/Ampleness/NefAmple.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.NefAmple.nonnegativeCone line 13
  2. theorem OAI.PiExponent.NefAmple.mem_nonnegativeCone line 23
  3. theorem OAI.PiExponent.NefAmple.isClosed_nonnegativeCone line 27
  4. theorem OAI.PiExponent.NefAmple.pos_smul_mem_interior line 37
  5. theorem OAI.PiExponent.NefAmple.add_mem_interior line 49
  6. theorem OAI.PiExponent.NefAmple.positive_combination_mem_interior line 59
  7. theorem OAI.PiExponent.NefAmple.combination_denominator_pos line 65
  8. theorem OAI.PiExponent.NefAmple.interpolation_divisor_identity line 72
  9. theorem OAI.PiExponent.NefAmple.interpolation_divisor_mem_interior line 89
  10. theorem OAI.PiExponent.NefAmple.interpolation_degree_margin line 101
  11. theorem OAI.PiExponent.NefAmple.interpolation_degree_pos line 114