OAI/Analysis/BoundedHochschild/AbelianProjectionForms.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Conversion between the two existing abelian-corner formulations.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.popa_abelian_of_finitePath line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.abelian_partialIso line 27