OAI/Analysis/IrrationalRotation/Spectral/QuasinilpotentNonscalar.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InvariantProjection.norm_root_smul_one line 16
2. theorem OAI.InvariantProjection.scalar_eq_zero_of_norm_root_tendsto line 21
3. theorem OAI.InvariantProjection.not_scalar_of_nonzero_norm_root_tendsto line 31
4. theorem OAI.InvariantProjection.continuousLinearMap_not_scalar_of_nonzero_norm_root_tendsto line 45