OAI/Analysis/SymmetricDomains/CoordinateFieldApply.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Biholomorph.ambientMap line 39
  2. theorem OAI.Release061.Biholomorph.ambientMap_apply line 42
  3. theorem OAI.Release061.Biholomorph.ambientMap_analytic line 45
  4. def OAI.Release061.Biholomorph.mapDerivative line 48
  5. theorem OAI.Release061.Biholomorph.mapDerivative_symm_comp line 51
  6. def OAI.Release061.Biholomorph.mapDerivativeEquiv line 65
  7. theorem OAI.Release061.Biholomorph.mapDerivativeEquiv_apply line 81
  8. def OAI.Release061.Biholomorph.coordinateField line 85
  9. theorem OAI.Release061.Biholomorph.coordinateField_apply line 90
  10. theorem OAI.Release061.Biholomorph.coordinateField_symm_cancel line 95
  11. theorem OAI.Release061.Biholomorph.infinitesimalGenerator_autTransport line 109
  12. theorem OAI.Release061.Biholomorph.IsCompleteGenerator.coordinateField line 137