OAI/Analysis/BoundedHochschild/FiniteCornerGroups.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite signed-permutation groups in proper corners, extended by the identity on the complement. Their spans contain every corner matrix unit.

  1. def OAI.BoundedHochschild.KadisonRingrose.finiteCornerGroupHom line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.corner_matrixUnit_mem_group_span line 22
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteCornerGroupHom_mem line 51