OAI/Analysis/JiangSu/TensorProducts/HilbertTensorCache.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ActualSpatial.tensorMap line 16
2. lemma OAI.ActualSpatial.tensorMap_tmul line 19
3. lemma OAI.ActualSpatial.tensorMap_dense line 20
4. lemma OAI.ActualSpatial.tensorMap_injective line 21
5. lemma OAI.ActualSpatial.leftHom_injective line 26