OAI/Analysis/IrrationalRotation/Spectral/QuasinilpotentTraceDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.inverse_one_sub_smul_mul_moment_zero line 12
2. theorem OAI.Invariant233.TracialState.inverse_one_sub_smul_mul_eq_zero line 26
3. theorem OAI.Invariant233.TracialState.inverse_one_sub_smul_mul_smul_eq_zero line 31
4. theorem OAI.Invariant233.TracialState.re_normalized_normSquare_differential_eq_zero line 37