OAI/Analysis/IrrationalRotation/Product/ProductFields.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.shiftOperator_ae line 15
2. theorem OAI.Invariant233.ProductModel.multiplier_ae line 19
3. theorem OAI.Invariant233.ProductModel.shiftOperator_commutes_multiplier line 26
4. theorem OAI.Invariant233.ProductModel.multiplier_commutes_scalar line 32
5. theorem OAI.Invariant233.ProductModel.scalarMultiplier_mem_commutant line 40
6. theorem OAI.Invariant233.ProductModel.factor_commutes_scalarMultiplier line 53
7. theorem OAI.Invariant233.ProductModel.exists_unique_field line 58