OAI/Analysis/Pureness/Tensor/AlgebraicQuotientTensorLift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.algebraicTensor_quotient_zero line 19
2. def OAI.CuntzPureness.algebraicQuotientTensorLift line 29
3. lemma OAI.CuntzPureness.algebraicQuotientTensorLift_map line 36
4. lemma OAI.CuntzPureness.algebraicQuotientTensorLift_dense line 42
5. lemma OAI.CuntzPureness.spatialTensorQuotientFactor_lift line 56
6. lemma OAI.CuntzPureness.algebraicQuotientTensorLift_injective line 65