OAI/Combinatorics/FiniteCircle/TreeBranching.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.TreeLeaf line 11
  2. instance OAI.FiniteCircle.treeLeafFintype line 15
  3. instance OAI.FiniteCircle.treeLeafDecidableEq line 21
  4. def OAI.FiniteCircle.treeCheap line 24
  5. theorem OAI.FiniteCircle.treeCheap_generator line 50
  6. theorem OAI.FiniteCircle.treeCheap_child line 55
  7. def OAI.FiniteCircle.treeFrequency line 70
  8. theorem OAI.FiniteCircle.treeFrequency_sum line 75
  9. theorem OAI.FiniteCircle.treeFrequency_mass line 87
  10. def OAI.FiniteCircle.flatMaskState line 99
  11. theorem OAI.FiniteCircle.flatMaskState_shift line 104
  12. def OAI.FiniteCircle.flatExcludedState line 113
  13. theorem OAI.FiniteCircle.flatExcludedState_shift line 118
  14. theorem OAI.FiniteCircle.char_sum line 127
  15. theorem OAI.FiniteCircle.character_dot line 135
  16. theorem OAI.FiniteCircle.character_dot_eq_one line 149
  17. theorem OAI.FiniteCircle.dot_restrict_child line 154
  18. theorem OAI.FiniteCircle.subcircle_intCast line 166
  19. theorem OAI.FiniteCircle.mask_generator_apply line 174
  20. def OAI.FiniteCircle.maskCheap line 195
  21. theorem OAI.FiniteCircle.mask_dot_generator line 200
  22. theorem OAI.FiniteCircle.mask_annihilator_congruences line 232
  23. theorem OAI.FiniteCircle.mask_character_branching line 263
  24. def OAI.FiniteCircle.ExcludedCongruences line 295
  25. theorem OAI.FiniteCircle.many_excluded_children line 303
  26. theorem OAI.FiniteCircle.excluded_branching_induction line 328
  27. theorem OAI.FiniteCircle.excluded_frequency_branching line 374
  28. theorem OAI.FiniteCircle.excluded_generator_apply line 391
  29. def OAI.FiniteCircle.excludedCheap line 411
  30. theorem OAI.FiniteCircle.excluded_dot_generator line 416
  31. theorem OAI.FiniteCircle.excluded_annihilator_congruences line 443
  32. theorem OAI.FiniteCircle.excluded_character_branching line 474