OAI/GroupTheory/SimpleOvergroups/PrefixProduct.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryPrefixOperators.Arithmetic.cancel line 10
  2. theorem OAI.BinaryPrefixOperators.Arithmetic.deletion_insertion line 16
  3. theorem OAI.BinaryPrefixOperators.Arithmetic.deletion_insertion_cancel line 36
  4. def OAI.BinaryPrefixOperators.Arithmetic.multiplyPair line 46
  5. theorem OAI.BinaryPrefixOperators.Arithmetic.replacement_mul line 50
  6. def OAI.BinaryPrefixOperators.Arithmetic.Lists.mulTerm line 64
  7. def OAI.BinaryPrefixOperators.Arithmetic.Lists.product line 67
  8. def OAI.BinaryPrefixOperators.Arithmetic.Lists.value line 70
  9. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_nil line 72
  10. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_cons line 73
  11. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_append line 76
  12. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_singleton line 79
  13. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_mulTerm line 82
  14. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_product line 87
  15. theorem OAI.BinaryPrefixOperators.Arithmetic.Lists.value_surjective line 102