OAI/Analysis/IrrationalRotation/Operators/ProjectionTraceRigidity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProjectionTraceRigidity.vectorTrace_eq_norm_sq line 15
2. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_gap_eq_norm_sq line 27
3. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_mono line 34
4. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_re_eq_zero_iff line 42
5. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_re_eq_iff_of_nested line 53
6. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_eq_iff_of_nested line 66
7. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_lt_of_nested_ne line 76
8. theorem OAI.Invariant233.ProjectionTraceRigidity.trace_re_eq_one_iff line 84
9. theorem OAI.Invariant233.ProjectionTraceRigidity.trivial_iff_of_trace_eq line 93