OAI/Analysis/IrrationalRotation/Operators/FieldOperator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.DirectIntegral.fieldOperator_ae line 22
2. theorem OAI.Invariant233.DirectIntegral.norm_fieldOperator_le line 26
3. theorem OAI.Invariant233.DirectIntegral.fieldOperator_congr line 31
4. theorem OAI.Invariant233.DirectIntegral.fieldOperator_comp_of_ae_eq line 40
5. theorem OAI.Invariant233.DirectIntegral.fieldOperator_ae_eq_of_eq line 57
6. theorem OAI.Invariant233.DirectIntegral.fieldOperator_adjoint_of_ae_eq line 85