OAI/Analysis/OperatorAlgebra/TracialStatePullback.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pullback of a tracial state by a unital star homomorphism.

  1. def OAI.WeakPureInfiniteness.tracialStatePullback line 14
  2. lemma OAI.WeakPureInfiniteness.tracialStatePullback_apply line 26
  3. lemma OAI.WeakPureInfiniteness.tracialStatePullback_faithful line 29