OAI/Analysis/KadisonKastler/FixedProductRepresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fixed tensor factor in an arbitrary separable representation

Choose the faithful cyclic representation only to prove the factor's type. Tensor functoriality and core independence transfer that conclusion back to the user's original represented algebra.

  1. theorem OAI.KadisonKastler.TwoRatioProductModel.tensor_typeIII1_general line 24