OAI/Analysis/Pureness/Tensor/ScalarMatrixTensor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.matrixStateScalarTensorHom line 15
2. lemma OAI.CuntzPureness.matrixStateScalarTensorHom_tmul line 21
3. lemma OAI.CuntzPureness.matrixStateScalarTensorHom_tmul_eq_zero line 26
4. lemma OAI.CuntzPureness.matrixStateScalarTensorHom_norm_square line 35
5. lemma OAI.CuntzPureness.matrixStateScalarTensorHom_sum_norm_le line 45