OAI/Analysis/KadisonKastler/ConjugatedMatrixInsertion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix insertion from a positive-vector comparison

A unitary commuting with the prescribed projection carries a matrix algebra containing that projection to another such matrix algebra. The quadratic vector transport supplies its actual central unit vector.

  1. theorem OAI.KadisonKastler.unitaryConjugateMatrixUnits_hom line 24
  2. theorem OAI.KadisonKastler.mem_unitaryConjugateMatrixUnits line 32
  3. theorem OAI.KadisonKastler.unitaryConjugateMatrixUnits_contains_projection line 38
  4. theorem OAI.KadisonKastler.exists_matrix_stage_of_conjugated_vector line 51