OAI/Analysis/SymmetricDomains/HeisenbergShiftAxis.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.Hermitian.heisenbergShift line 37
2. theorem OAI.Release061.Hermitian.heisenbergShift_residual line 44
3. lemma OAI.Release061.Hermitian.heisenbergShift_mem line 59
4. def OAI.Release061.Hermitian.hermLinearLeft line 69
5. lemma OAI.Release061.Hermitian.heisenbergShift_analytic line 74
6. lemma OAI.Release061.Hermitian.hermPart_neg_right line 90
7. lemma OAI.Release061.Hermitian.heisenbergShift_left_inverse line 96
8. def OAI.Release061.Hermitian.heisenbergHomeomorph line 113
9. def OAI.Release061.Hermitian.heisenbergModelHomeomorph line 125
10. theorem OAI.Release061.Hermitian.heisenbergShift_axis line 132