OAI/Analysis/Pureness/GroupAlgebra/FreeGroupTensorTrace.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spatialFreeRowPolynomial line 17
2. lemma OAI.CuntzPureness.spatialFreeRowPolynomial_coe line 24
3. theorem OAI.CuntzPureness.spatialFreeTensor_nonunitary_isometry line 41
4. theorem OAI.CuntzPureness.tracialState_of_finite_freeGroup_tensor line 73