OAI/Analysis/SymmetricDomains/OneKernel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.Biholomorph.WeightedLieModel.jet line 53
2. def OAI.Release061.Biholomorph.WeightedLieModel.firstJet line 54
3. theorem OAI.Release061.Biholomorph.WeightedLieModel.euler_jet line 56
4. theorem OAI.Release061.Biholomorph.WeightedLieModel.rotation_jet line 62
5. theorem OAI.Release061.Biholomorph.WeightedLieModel.eigen_jet_zero line 68
6. theorem OAI.Release061.Biholomorph.WeightedLieModel.centered_value_zero line 77
7. theorem OAI.Release061.Biholomorph.WeightedLieModel.centered_firstJet_one_zero line 85
8. theorem OAI.Release061.Biholomorph.WeightedLieModel.centered_half_rotation_firstJet line 96
9. theorem OAI.Release061.Biholomorph.WeightedLieModel.centered_rotation_value line 120
10. theorem OAI.Release061.Biholomorph.WeightedLieModel.ofReal_eigen line 128
11. theorem OAI.Release061.Biholomorph.WeightedLieModel.center_of_commutes line 133
12. theorem OAI.Release061.Biholomorph.WeightedLieModel.real_zero_of_zero_jet line 136
13. theorem OAI.Release061.Biholomorph.WeightedLieModel.half_real_kernel line 144
14. theorem OAI.Release061.Biholomorph.WeightedLieModel.half_kernel line 163
15. theorem OAI.Release061.Biholomorph.WeightedLieModel.bracket_translation_eigen line 173
16. theorem OAI.Release061.Biholomorph.WeightedLieModel.one_real_kernel line 179
17. theorem OAI.Release061.Biholomorph.WeightedLieModel.one_kernel line 206