OAI/Analysis/WeakInfiniteness/CentralCopiesTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.ApproximatelyCentralCopies line 28
2. def OAI.WeakPureInfiniteness.tensorCopyMap line 34
3. lemma OAI.WeakPureInfiniteness.tensorCopyMap_elementary line 37
4. lemma OAI.WeakPureInfiniteness.tensorCopyMap_polynomial_commutator line 42
5. lemma OAI.WeakPureInfiniteness.norm_tensorCopyMap_polynomial_commutator_le line 57
6. lemma OAI.WeakPureInfiniteness.norm_commutator_perturb_le line 75
7. lemma OAI.WeakPureInfiniteness.ApproximatelyCentralCopies.tensor_commutator line 86