OAI/Analysis/SymmetricDomains/AdNilpotentPositiveDilations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Biholomorph.translationAut line 37
  2. theorem OAI.Release061.Biholomorph.translationAut_apply line 45
  3. theorem OAI.Release061.Biholomorph.translationAut_inv_apply line 49
  4. theorem OAI.Release061.Biholomorph.translationAut_zero line 53
  5. theorem OAI.Release061.Biholomorph.translationAut_add line 60
  6. theorem OAI.Release061.Biholomorph.continuous_translationAut line 69
  7. def OAI.Release061.Biholomorph.linearAut line 78
  8. theorem OAI.Release061.Biholomorph.linearAut_apply line 87
  9. theorem OAI.Release061.Biholomorph.linearAut_inv_apply line 91
  10. theorem OAI.Release061.Biholomorph.linearAut_translation_conjugate line 95
  11. theorem OAI.LinearMap.isNilpotent_of_positive_smul_conjugate line 113
  12. theorem OAI.LinearMap.isNilpotent_of_positive_smul_conjugate_algebraic line 140
  13. theorem OAI.LieAlgebra.ad_isNilpotent_of_positive_dilations line 163