OAI/Analysis/JiangSu/Absorption/TensorIdealAbsorption.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NonunitalTensor.original_left_mul line 19
2. lemma OAI.NonunitalTensor.span_left_elementary line 27
3. lemma OAI.NonunitalTensor.ideal_left_elementary line 47
4. lemma OAI.NonunitalTensor.ideal_left_absorb line 60
5. lemma OAI.NonunitalTensor.ideal_right_absorb line 69
6. instance OAI.NonunitalTensor.tensorIdeal_separable line 88
7. def OAI.NonunitalTensor.originalInclusion line 100
8. lemma OAI.NonunitalTensor.originalInclusion_isometry line 106
9. theorem OAI.NonunitalTensor.equiv_of_embedding line 122