OAI/Analysis/SymmetricDomains/PositiveVertexJets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LieAlgebra.innerExp_apply_of_cube_zero line 53
2. theorem OAI.Release061.Biholomorph.WeightedLieModel.field_euler_value line 77
3. theorem OAI.Release061.Biholomorph.WeightedLieModel.field_translation_value line 80
4. theorem OAI.Release061.Biholomorph.WeightedLieModel.field_rotation_value line 83
5. theorem OAI.Release061.Biholomorph.WeightedLieModel.firstJet_euler line 86
6. theorem OAI.Release061.Biholomorph.WeightedLieModel.firstJet_translation line 90
7. theorem OAI.Release061.Biholomorph.WeightedLieModel.firstJet_rotation line 94
8. theorem OAI.Release061.Biholomorph.WeightedLieModel.ofReal_smul line 98
9. theorem OAI.Release061.Biholomorph.WeightedLieModel.positive_vertex_jets line 103