OAI/Analysis/SymmetricDomains/HorizontalGraphComplexification.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Flatten.realEmbedding line 33
  2. def OAI.Release061.Flatten.realPart line 36
  3. def OAI.Release061.Flatten.imaginaryPart line 39
  4. lemma OAI.Release061.Flatten.complexLinear_zero_of_real line 42
  5. lemma OAI.Release061.Flatten.complexification_deriv_zero line 56
  6. theorem OAI.Release061.Flatten.real_analytic_local_inverse line 74
  7. theorem OAI.Release061.Flatten.horizontal_graph_complexification line 95