OAI/Analysis/IrrationalRotation/Spectral/PolarFactor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.PolarFactor.star_mul_self_unitary_mul line 12
2. theorem OAI.Invariant233.PolarFactor.abs_unitary_mul line 21
3. theorem OAI.Invariant233.PolarFactor.abs_unitary_mul_of_nonneg line 26
4. theorem OAI.Invariant233.PolarFactor.norm_unitary_mul line 31
5. theorem OAI.Invariant233.PolarFactor.ker_unitary_mul line 35
6. theorem OAI.Invariant233.PolarFactor.unitary_mul_ne_zero line 46
7. theorem OAI.Invariant233.PolarFactor.denseRange_of_nonneg_ker_eq_bot line 53
8. theorem OAI.Invariant233.PolarFactor.unitary_factor_unique_of_nonneg_ker_eq_bot line 60