OAI/Analysis/BoundedHochschild/FlipMatrixNesting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exchange the finite matrix indices in a two-by-two amplification.

  1. def OAI.BoundedHochschild.KadisonRingrose.flipMatrixNesting line 13
  2. lemma OAI.BoundedHochschild.KadisonRingrose.flipMatrixNesting_apply line 30