CPFaithfulRestriction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Complete positivity can be tested after a faithful star homomorphism. This lets an operator-valued cpc projection be viewed as a map into its actual closed commutant algebra.

lemma OAI.WeakPureInfiniteness.completelyPositive_of_faithful_postcomp line 18