OAI/NumberTheory/PiExponent/Jets/BranchContact.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.BranchContact.active line 10
  2. theorem OAI.PiExponent.BranchContact.mem_active line 14
  3. theorem OAI.PiExponent.BranchContact.active_nonempty line 19
  4. def OAI.PiExponent.BranchContact.contact line 24
  5. theorem OAI.PiExponent.BranchContact.contact_le line 27
  6. theorem OAI.PiExponent.BranchContact.exists_attains line 32
  7. theorem OAI.PiExponent.BranchContact.contact_pos line 38
  8. theorem OAI.PiExponent.BranchContact.contact_bound line 49
  9. theorem OAI.PiExponent.BranchContact.le_contact line 58
  10. theorem OAI.PiExponent.BranchContact.order_add_lower line 67
  11. theorem OAI.PiExponent.BranchContact.exists_attaining_add line 87
  12. theorem OAI.PiExponent.BranchContact.add_not_all_zero line 112
  13. theorem OAI.PiExponent.BranchContact.contact_add_high_tail line 119