OAI/GroupTheory/SimpleAmenable/CentralCovers/AtomConjugation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.difference_conjugation_of_atom line 15
  2. theorem OAI.SimpleAmenable.centralLaw_of_atom_conjugations line 30
  3. def OAI.SimpleAmenable.LocalCentralLaw line 52
  4. theorem OAI.SimpleAmenable.local_null_is_central line 56
  5. theorem OAI.SimpleAmenable.local_equality_mod_center line 71
  6. abbrev OAI.SimpleAmenable.SwapLabel line 93
  7. def OAI.SimpleAmenable.reserveAtom line 96
  8. theorem OAI.SimpleAmenable.swapLabel_inv line 100
  9. theorem OAI.SimpleAmenable.reserveAtom_base line 104
  10. theorem OAI.SimpleAmenable.reserveAtom_difference line 110
  11. theorem OAI.SimpleAmenable.reserveAtoms_generate line 117
  12. def OAI.SimpleAmenable.swapLabelConj line 136
  13. theorem OAI.SimpleAmenable.reserveAtom_conjugation line 143