OAI/GroupTheory/SimpleOvergroups/PrefixArithmetic.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryPrefixOperators.Arithmetic.Word line 11
  2. abbrev OAI.BinaryPrefixOperators.Arithmetic.Pair line 12
  3. def OAI.BinaryPrefixOperators.Arithmetic.insertion line 17
  4. def OAI.BinaryPrefixOperators.Arithmetic.deletion line 21
  5. theorem OAI.BinaryPrefixOperators.Arithmetic.prefix_nil line 25
  6. theorem OAI.BinaryPrefixOperators.Arithmetic.prefix_cons line 26
  7. theorem OAI.BinaryPrefixOperators.Arithmetic.deletion_nil line 28
  8. theorem OAI.BinaryPrefixOperators.Arithmetic.deletion_cons line 29
  9. theorem OAI.BinaryPrefixOperators.Arithmetic.prefix_append line 32
  10. theorem OAI.BinaryPrefixOperators.Arithmetic.deletion_append line 34
  11. theorem OAI.BinaryPrefixOperators.Arithmetic.prefix_single line 38
  12. theorem OAI.BinaryPrefixOperators.Arithmetic.deletion_single line 48
  13. def OAI.BinaryPrefixOperators.Arithmetic.replacement line 63
  14. theorem OAI.BinaryPrefixOperators.Arithmetic.replacement_single line 65
  15. theorem OAI.BinaryPrefixOperators.Arithmetic.replacement_domain line 73
  16. theorem OAI.BinaryPrefixOperators.Arithmetic.split_replacement line 82
  17. def OAI.BinaryPrefixOperators.Arithmetic.marker line 92
  18. theorem OAI.BinaryPrefixOperators.Arithmetic.marker_after line 94
  19. theorem OAI.BinaryPrefixOperators.Arithmetic.marker_separates line 97
  20. def OAI.BinaryPrefixOperators.Arithmetic.evaluate line 113
  21. theorem OAI.BinaryPrefixOperators.Arithmetic.evaluate_single line 116
  22. theorem OAI.BinaryPrefixOperators.Arithmetic.coefficient_test line 120
  23. theorem OAI.BinaryPrefixOperators.Arithmetic.evaluate_eq_zero_of_depth line 150
  24. def OAI.BinaryPrefixOperators.Arithmetic.subdivide line 167
  25. theorem OAI.BinaryPrefixOperators.Arithmetic.evaluate_subdivide line 171
  26. theorem OAI.BinaryPrefixOperators.Arithmetic.subdivide_depth line 179
  27. def OAI.BinaryPrefixOperators.Arithmetic.uniform line 194
  28. theorem OAI.BinaryPrefixOperators.Arithmetic.uniform_single line 197
  29. theorem OAI.BinaryPrefixOperators.Arithmetic.evaluate_uniform line 201
  30. theorem OAI.BinaryPrefixOperators.Arithmetic.uniform_depth line 209
  31. def OAI.BinaryPrefixOperators.Arithmetic.domainDepth line 221
  32. theorem OAI.BinaryPrefixOperators.Arithmetic.finite_zero_test line 223