OAI/Analysis/BoundedHochschild/CentralBlockUnitaries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite groups assembled across finite central partitions.

  1. def OAI.BoundedHochschild.KadisonRingrose.centralBlock line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_mul line 24
  3. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_star line 42
  4. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_one line 50
  5. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_mem_unitary line 56
  6. def OAI.BoundedHochschild.KadisonRingrose.centralBlockHom line 66