OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Splice.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OrdinaryCorrelations.ArithmeticSaving.Unselected line 19
  2. def OAI.OrdinaryCorrelations.ArithmeticSaving.splice line 21
  3. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.splice_selected line 24
  4. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.splice_unselected line 31
  5. def OAI.OrdinaryCorrelations.ArithmeticSaving.assignmentEquiv line 34
  6. def OAI.OrdinaryCorrelations.ArithmeticSaving.prefixSplice line 46
  7. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.prefixSplice_agrees line 50
  8. structure OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions line 61
  9. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.support_agrees line 73
  10. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.modulus_agrees line 87
  11. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.coefficient_agrees line 101
  12. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.constant_agrees line 108
  13. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.divisor_agrees line 115
  14. def OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.clause line 126
  15. lemma OAI.OrdinaryCorrelations.ArithmeticSaving.TriangularExpressions.clause_actual line 133