OAI/GroupTheory/SimpleAmenable/CentralCovers/DirectFactors.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.CommutingFactors line 14
  2. theorem OAI.SimpleAmenable.CommutingFactors.symm line 21
  3. theorem OAI.SimpleAmenable.CommutingFactors.mem_center_of_mem_inter line 27
  4. theorem OAI.SimpleAmenable.CommutingFactors.inter_eq_bot line 34
  5. theorem OAI.SimpleAmenable.CommutingFactors.mem_left_of_commute_right line 40
  6. def OAI.SimpleAmenable.CommutingFactors.productHom line 62
  7. theorem OAI.SimpleAmenable.CommutingFactors.productHom_apply line 74
  8. theorem OAI.SimpleAmenable.CommutingFactors.productHom_bijective line 77
  9. def OAI.SimpleAmenable.CommutingFactors.productEquiv line 95
  10. theorem OAI.SimpleAmenable.CommutingFactors.productEquiv_apply line 99
  11. theorem OAI.SimpleAmenable.CommutingFactors.left_component_commutes line 103
  12. theorem OAI.SimpleAmenable.CommutingFactors.refine_four line 116