OAI/Analysis/SymmetricDomains/ModelNormalTranslationAd.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.Biholomorph.generator_ad_isNilpotent_of_scaled_flow line 48
  2. def OAI.Release061.Biholomorph.weightedScaleCLE line 67
  3. theorem OAI.Release061.Biholomorph.weightedScaleCLE_apply line 76
  4. def OAI.Release061.Biholomorph.flatWeightedScale line 79
  5. theorem OAI.Release061.Biholomorph.flatWeightedScale_mem line 84
  6. def OAI.Release061.Biholomorph.flatNormalVector line 99
  7. theorem OAI.Release061.Biholomorph.flatNormal_translation_mem line 102
  8. theorem OAI.Release061.Biholomorph.flatWeightedScale_normal line 123
  9. theorem OAI.Release061.Biholomorph.model_normal_translation_ad_nilpotent line 133