OAI/Analysis/KadisonKastler/CommonReducingProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Aligning a reducing projection while fixing the common algebra

  1. theorem OAI.KadisonKastler.exists_commutant_projection_of_finite_gap line 25
  2. theorem OAI.KadisonKastler.exists_unitary_aligning_common_reducing_projection line 52