OAI/Analysis/OperatorAlgebra/TotalTensorVectors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Testing operators on tensor products of two total families of vectors.

  1. theorem OAI.WeakPureInfiniteness.completed_tensor_operator_eq_zero line 18