OAI/Analysis/IrrationalRotation/Product/ProductHilbert.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Invariant233.ProductModel.hilbert_separable line 9
2. theorem OAI.Invariant233.ProductModel.hilbert_not_finiteDimensional line 12
3. instance OAI.Invariant233.ProductModel.hilbert_nontrivial line 15
4. theorem OAI.Invariant233.ProductModel.norm_traceVector line 22
5. theorem OAI.Invariant233.ProductModel.traceVector_inner_one line 26