OAI/Analysis/KadisonKastler/FactorProjectionSeparatesCommutant.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nonzero factor projection separates its commutant

This is the faithfulness needed when reducing the semifinite spatial splitting problem to a finite corner.

  1. theorem OAI.KadisonKastler.commutant_eq_zero_of_mul_factor_projection line 20