OAI/Analysis/BoundedHochschild/FactorizedProjectionDefects.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The right-module defect at a projection is an off-diagonal coefficient of the fixed operator factorization.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.factorized_projection_defect line 16