OAI/Analysis/SymmetricDomains/AnalyticSecondJetCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearMap.diagonal_coordinate_pow line 44
  2. theorem OAI.LinearMap.diagonal_coordinate_aeval line 52
  3. theorem OAI.LinearMap.diagonal_faithful_aeval_eq_zero line 62
  4. theorem OAI.LinearMap.diagonal_faithful_isSemisimple line 75
  5. theorem OAI.LinearMap.diagonal_faithful_eigenvalue_mem line 82
  6. abbrev OAI.SecondJetIndex line 102
  7. def OAI.secondJetWeight line 104
  8. def OAI.analyticSecondJetCoordinates line 114
  9. theorem OAI.analyticSecondJetCoordinates_eq_zero_iff line 129
  10. theorem OAI.analyticSecondJetCoordinates_injective line 157
  11. theorem OAI.basis_coordinate_diagonal line 166
  12. theorem OAI.analyticSecondJetCoordinates_euler line 181