OAI/Analysis/IrrationalRotation/Rotation/RepresentedPositiveDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.DirectIntegral.ae_invariant_of_represented_invariant line 17
2. theorem OAI.Invariant233.DirectIntegral.ae_isStarProjection_of_representation line 41
3. theorem OAI.Invariant233.DirectIntegral.real_constant_vector_state_eq_integral line 59
4. theorem OAI.Invariant233.Fields.ae_strict_diagonal_of_represented_weighted_shift line 81