OAI/Analysis/BoundedHochschild/ProjectionModuleMaps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of the diagonal projection defects implies the full right module identity, by the density of the span of projections.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.right_module_on_projections line 17
  2. theorem OAI.BoundedHochschild.KadisonRingrose.right_module_of_projection_defects line 29