OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedSupportReductionGuards.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.frequencies line 10
  2. theorem OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.toHistory_root line 14
  3. theorem OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.toHistory_frequencies line 16
  4. def OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.RootData line 23
  5. def OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.LocalTests line 30
  6. def OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.NodeRelations line 38
  7. theorem OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.rootData_iff_projection line 48
  8. theorem OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.localTests_iff_projection line 53
  9. lemma OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.toNat_eq_iff line 60
  10. theorem OAI.Ostmann.Arithmetic.HistorySignedSupportReduction.nodeRelations_iff_projection line 62