OAI/Combinatorics/Chromatic/Walls/PrimitiveStrings.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.PrimitiveStrings.Strings line 12
  2. def OAI.ElementaryPositivity.PrimitiveStrings.evaluate line 14
  3. theorem OAI.ElementaryPositivity.PrimitiveStrings.evaluate_single line 17
  4. def OAI.ElementaryPositivity.PrimitiveStrings.differentiate line 21
  5. def OAI.ElementaryPositivity.PrimitiveStrings.integrate line 27
  6. theorem OAI.ElementaryPositivity.PrimitiveStrings.differentiate_single_zero line 30
  7. theorem OAI.ElementaryPositivity.PrimitiveStrings.differentiate_single_succ line 33
  8. theorem OAI.ElementaryPositivity.PrimitiveStrings.integrate_single line 37
  9. theorem OAI.ElementaryPositivity.PrimitiveStrings.differentiate_apply line 41
  10. theorem OAI.ElementaryPositivity.PrimitiveStrings.differentiate_integrate line 54
  11. theorem OAI.ElementaryPositivity.PrimitiveStrings.derivative_string line 64
  12. theorem OAI.ElementaryPositivity.PrimitiveStrings.evaluate_differentiate line 74
  13. theorem OAI.ElementaryPositivity.PrimitiveStrings.evaluate_injective_bounded line 84
  14. theorem OAI.ElementaryPositivity.PrimitiveStrings.evaluate_injective line 109
  15. theorem OAI.ElementaryPositivity.PrimitiveStrings.exists_strings_of_pow_eq_zero line 119
  16. def OAI.ElementaryPositivity.PrimitiveStrings.decomposition line 139