OAI/Analysis/BoundedHochschild/CentralBlockSpans.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Matrix coefficients in the span of finite block unitary groups.

  1. def OAI.BoundedHochschild.KadisonRingrose.centralBlockSpan line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_unitary_mem_span line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_component_mem_span line 27
  4. lemma OAI.BoundedHochschild.KadisonRingrose.centralBlock_mul_mem_span line 47