OAI/Analysis/KadisonKastler/StateScalingFiniteSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite orthogonal sums of state-scaling partial isometries

  1. theorem OAI.KadisonKastler.StateScales.sum line 17
  2. theorem OAI.KadisonKastler.partialIsometry_sum_coisometry line 27