OAI/Analysis/WeakInfiniteness/NonUnitalGroupTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.completedGroupOperator line 22
2. lemma OAI.WeakPureInfiniteness.completedGroupOperator_one line 25
3. lemma OAI.WeakPureInfiniteness.completedGroupOperator_mul line 29
4. lemma OAI.WeakPureInfiniteness.completedGroupOperator_inv line 41
5. lemma OAI.WeakPureInfiniteness.completedGroupOperator_unitary line 48
6. def OAI.WeakPureInfiniteness.completedGroupUnitary line 56
7. lemma OAI.WeakPureInfiniteness.projection_mul_completedGroup line 61
8. theorem OAI.WeakPureInfiniteness.norm_freeTensor_nonunital_sum_le line 68