OAI/Analysis/IrrationalRotation/Rotation/RotationTrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.Rotation.algebra_commutes_shiftedPullback_int line 13
2. theorem OAI.Invariant233.Rotation.field_covariance_int line 48
3. theorem OAI.Invariant233.Rotation.exists_covariant_field line 63
4. theorem OAI.Invariant233.Rotation.vacuumFunctional_eq_integral_of_field line 76
5. theorem OAI.Invariant233.Rotation.vacuum_faithfulTracial line 84