OAI/Analysis/SymmetricDomains/InnerExp.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Release061.Biholomorph.ComplexGenerators line 49
  2. def OAI.Release061.Biholomorph.complexGeneratorField line 51
  3. theorem OAI.Release061.Biholomorph.complexGeneratorField_tmul line 55
  4. theorem OAI.Release061.Biholomorph.complexGeneratorField_analytic line 58
  5. theorem OAI.Release061.Biholomorph.complexGeneratorField_zero_outside line 65
  6. theorem OAI.Release061.Biholomorph.complexGeneratorField_secondJet_injective line 71
  7. theorem OAI.Release061.Biholomorph.complexGeneratorField_injective line 83
  8. def OAI.LieAlgebra.leftInner line 102
  9. theorem OAI.LieAlgebra.leftInner_apply line 109
  10. theorem OAI.LieAlgebra.leftInner_toLinearMap line 111
  11. def OAI.LieAlgebra.innerExp line 116
  12. theorem OAI.LieAlgebra.innerExp_apply_of_square_zero line 119
  13. theorem OAI.LieAlgebra.innerExp_euler line 132
  14. theorem OAI.LieAlgebra.innerExp_fixed line 136