OAI/NumberTheory/Ostmann/Construction/FixedPivotTopConditions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Original-prime tests for a top atom pair containing a fixed pivot

  1. def OAI.Ostmann.TopPrimeCondition.HasVariable line 13
  2. def OAI.Ostmann.TopPrimeCondition.fixPivot line 18
  3. theorem OAI.Ostmann.TopPrimeCondition.fixPivot_holds line 27
  4. theorem OAI.Ostmann.TopPrimeCondition.fixPivot_bounded line 44
  5. theorem OAI.Ostmann.atomPairChecks_hasVariable line 65
  6. theorem OAI.Ostmann.insertedConstituentWord_none line 81
  7. theorem OAI.Ostmann.insertedConstituentWord_none_unique line 95
  8. theorem OAI.Ostmann.insertedAtomPairChecks_hasVariable line 106
  9. theorem OAI.Ostmann.none_mem_option_map_iff line 112
  10. theorem OAI.Ostmann.insertedPermutedAtomPairChecks_hasVariable line 123
  11. def OAI.Ostmann.fixedPivotCheckAt line 136
  12. theorem OAI.Ostmann.fixedPivotCheckAt_all line 141
  13. theorem OAI.Ostmann.fixedPivotCheckAt_bounded line 153