OAI/Analysis/JiangSu/TensorProducts/StarTensorMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Pureness.starTensorMap line 15
2. lemma OAI.Pureness.starTensorMap_tmul line 25
3. lemma OAI.Pureness.starTensorMap_injective line 27
4. def OAI.Pureness.tensorLeft line 31
5. def OAI.Pureness.tensorRight line 37
6. lemma OAI.Pureness.tensorLeft_apply line 43
7. lemma OAI.Pureness.tensorRight_apply line 45