OAI/GroupTheory/SimpleAmenable/PolygonGeometry/NestedCutCalculus.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.commute_ratio_of_conjugation line 13
  2. def OAI.SimpleAmenable.differenceHom line 19
  3. theorem OAI.SimpleAmenable.differenceHom_apply line 30
  4. theorem OAI.SimpleAmenable.split_conjugation line 34
  5. theorem OAI.SimpleAmenable.nested_cut_commute_ratio line 41
  6. theorem OAI.SimpleAmenable.nested_cut_difference line 60
  7. theorem OAI.SimpleAmenable.ordered_differences_telescope line 71
  8. theorem OAI.SimpleAmenable.difference_commutes_with_prefix line 79
  9. theorem OAI.SimpleAmenable.same_conj_iff line 91
  10. theorem OAI.SimpleAmenable.commute_of_conditional_move line 108
  11. theorem OAI.SimpleAmenable.commutator_four line 113
  12. theorem OAI.SimpleAmenable.four_factor_in_subgroup line 130
  13. def OAI.SimpleAmenable.SameActionOn line 149
  14. theorem OAI.SimpleAmenable.intersection_control line 152
  15. theorem OAI.SimpleAmenable.conj_mul_of_commute line 195
  16. def OAI.SimpleAmenable.cutDifference line 206
  17. theorem OAI.SimpleAmenable.cutDifference_commute_prefix line 211
  18. theorem OAI.SimpleAmenable.cutDifference_pairwise line 223
  19. theorem OAI.SimpleAmenable.cutDifference_telescope line 229