OAI/Analysis/SymmetricDomains/FiniteDimensionalCompleteGenerator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.Biholomorph.infinitesimalGenerator_of_not_mem line 38
  2. theorem OAI.Release061.Biholomorph.infinitesimalGenerator_one line 42
  3. theorem OAI.Release061.Biholomorph.infinitesimalGenerator_hasDerivAt line 47
  4. theorem OAI.Release061.Biholomorph.infinitesimalGenerator_time_smul line 57
  5. def OAI.Release061.Biholomorph.IsCompleteGenerator line 69
  6. lemma OAI.Release061.Biholomorph.IsCompleteGenerator.analyticOnNhd line 73
  7. lemma OAI.Release061.Biholomorph.IsCompleteGenerator.eq_zero_of_not_mem line 79
  8. def OAI.Release061.Biholomorph.completeGeneratorSpace line 91
  9. def OAI.Release061.Biholomorph.completeGeneratorFirstJet line 109
  10. theorem OAI.Release061.Biholomorph.completeGeneratorFirstJet_injective line 122
  11. theorem OAI.Release061.Biholomorph.finiteDimensional_completeGeneratorSpace line 142