OAI/Analysis/Pureness/Tensor/SpatialCreationVacuum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spatialVacuumVector line 12
2. lemma OAI.CuntzPureness.spatialVacuumVector_norm line 16
3. theorem OAI.CuntzPureness.spatialFreeCreationSum_star_vacuum line 20
4. theorem OAI.CuntzPureness.operator_not_isUnit_of_star_kills line 32
5. theorem OAI.CuntzPureness.spatialFreeCreationSum_not_isUnit line 42