OAI/GroupTheory/SimpleOvergroups/PrefixLists.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryPrefixOperators.Arithmetic.Lists.Poly line 11
  2. def OAI.BinaryPrefixOperators.Arithmetic.Lists.toArray line 15
  3. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.toArray_nil line 19
  4. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.toArray_cons line 20
  5. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.toArray_append line 22
  6. def OAI.BinaryPrefixOperators.Arithmetic.Lists.coefficient line 27
  7. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.coefficient_nil line 30
  8. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.coefficient_cons line 31
  9. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.coefficient_eq line 34
  10. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.coefficient_eq_zero_of_not_mem line 39
  11. def OAI.BinaryPrefixOperators.Arithmetic.Lists.isZero line 49
  12. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.isZero_iff line 52
  13. def OAI.BinaryPrefixOperators.Arithmetic.Lists.suffixes line 66
  14. def OAI.BinaryPrefixOperators.Arithmetic.Lists.expandTerm line 70
  15. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.expandTerm_zero line 73
  16. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.expandTerm_succ line 77
  17. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.toArray_expandTerm line 83
  18. def OAI.BinaryPrefixOperators.Arithmetic.Lists.depth line 91
  19. def OAI.BinaryPrefixOperators.Arithmetic.Lists.spread line 95
  20. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.toArray_spread line 98
  21. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.depth_bound line 107
  22. def OAI.BinaryPrefixOperators.Arithmetic.Lists.zeroTest line 119
  23. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.zeroTest_iff line 121