OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairRows.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Arithmetic.HistoryPairRows.Occurrences line 14
  2. def OAI.Ostmann.Arithmetic.HistoryPairRows.level line 16
  3. def OAI.Ostmann.Arithmetic.HistoryPairRows.slot line 19
  4. def OAI.Ostmann.Arithmetic.HistoryPairRows.row line 22
  5. def OAI.Ostmann.Arithmetic.HistoryPairRows.leftFlag line 30
  6. def OAI.Ostmann.Arithmetic.HistoryPairRows.rightFlag line 34
  7. def OAI.Ostmann.Arithmetic.HistoryPairRows.minorFlag line 38
  8. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.row_above line 43
  9. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.flags_above line 53
  10. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.minorFlag_above line 61
  11. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.row_regular_nonzero line 69
  12. def OAI.Ostmann.Arithmetic.HistoryPairRows.AncestorUnits line 81
  13. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.row_regular_nonzero_field line 89
  14. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.flags_nonzero_field line 107
  15. def OAI.Ostmann.Arithmetic.HistoryPairRows.degreeBudget line 116
  16. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.row_atomCount line 120
  17. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.flag_degrees line 132
  18. theorem OAI.Ostmann.Arithmetic.HistoryPairRows.minorFlag_degree line 140