OAI/Analysis/SymmetricDomains/ImagPartLieReal.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Complexification.realPart line 46
  2. def OAI.Complexification.imagPart line 49
  3. def OAI.Complexification.ofReal line 52
  4. theorem OAI.Complexification.realPart_tmul line 54
  5. theorem OAI.Complexification.imagPart_tmul line 55
  6. theorem OAI.Complexification.ofReal_apply line 56
  7. theorem OAI.Complexification.realPart_ofReal line 57
  8. theorem OAI.Complexification.imagPart_ofReal line 58
  9. theorem OAI.Complexification.ofReal_injective line 60
  10. theorem OAI.Complexification.normalForm line 63
  11. theorem OAI.Complexification.ext line 67
  12. theorem OAI.Complexification.realPart_I_smul line 71
  13. theorem OAI.Complexification.imagPart_I_smul line 74
  14. theorem OAI.Complexification.realPart_real_smul line 78
  15. theorem OAI.Complexification.imagPart_real_smul line 82
  16. theorem OAI.Complexification.ofReal_lie line 89
  17. theorem OAI.Complexification.ad_ofReal_baseChange line 92
  18. theorem OAI.Complexification.ad_ofReal_nilpotent line 97
  19. theorem OAI.Complexification.realPart_lie_ofReal line 102
  20. theorem OAI.Complexification.imagPart_lie_ofReal line 106
  21. theorem OAI.Complexification.realPart_eigen line 111
  22. theorem OAI.Complexification.imagPart_eigen line 114
  23. theorem OAI.Complexification.eigen_eq_zero_of_imaginary_bracket line 118