OAI/Probability/FreeIsing/Trees/Transitivity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.TreeAut.refl line 11
  2. def OAI.Problem367.TreeAut.symm line 15
  3. def OAI.Problem367.TreeAut.trans line 22
  4. def OAI.Problem367.prefixFlipWord line 30
  5. theorem OAI.Problem367.prefixFlipWord_chain line 34
  6. theorem OAI.Problem367.prefixFlipWord_involutive line 46
  7. def OAI.Problem367.prefixFlip line 61
  8. theorem OAI.Problem367.prefixFlip_twice line 64
  9. theorem OAI.Problem367.prefixFlipWord_append_adj line 69
  10. theorem OAI.Problem367.prefixFlip_adj line 86
  11. def OAI.Problem367.prefixTreeAut line 92
  12. theorem OAI.Problem367.exists_treeAut_to_root line 107
  13. theorem OAI.Problem367.exists_treeAut_map line 123
  14. theorem OAI.Problem367.treeAut_transitive line 132
  15. theorem OAI.Problem367.exists_treeAut_swap_of_adj line 136