OAI/Analysis/SymmetricDomains/AnalyticDirectionalDerivationFun.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.germDirectionalDerivative line 33
  2. theorem OAI.Release061.germDirectionalDerivative_ofFun line 39
  3. def OAI.Release061.analyticDirectionalDerivative line 43
  4. def OAI.Release061.analyticDirectionalDerivation line 50
  5. abbrev OAI.Release061.MeromorphicGermField line 83
  6. def OAI.Release061.analyticGermOf line 85
  7. theorem OAI.Release061.analyticGermOf_eq_iff line 88
  8. theorem OAI.Release061.analyticDirectionalDerivation_ofFun line 93