OAI/Analysis/SymmetricDomains/ScalarPointSymmetryMap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Hermitian.scalarNormalCoordinates line 37
  2. lemma OAI.Release061.Hermitian.scalarNormalCoordinates_apply line 41
  3. lemma OAI.Release061.Hermitian.scalarNormalCoordinates_symm_apply line 45
  4. lemma OAI.Release061.Hermitian.scalar_hermQuadratic_homogeneous line 49
  5. lemma OAI.Release061.Hermitian.scalarNormalCoordinates_mem line 58
  6. def OAI.Release061.Hermitian.scalarAxisNormalization line 65
  7. lemma OAI.Release061.Hermitian.scalarAxisNormalization_apply line 71
  8. lemma OAI.Release061.Hermitian.scalarAxisNormalization_mem line 79
  9. lemma OAI.Release061.Hermitian.scalarAxisNormalization_analytic line 88
  10. lemma OAI.Release061.Hermitian.scalarAxisNormalization_inverse_analytic line 96
  11. def OAI.Release061.Hermitian.scalarPointSymmetryMap line 104
  12. lemma OAI.Release061.Hermitian.scalarPointSymmetryMap_mem line 109
  13. lemma OAI.Release061.Hermitian.scalarPointSymmetryMap_involutive line 122
  14. lemma OAI.Release061.Hermitian.scalarPointSymmetryMap_analytic line 133
  15. lemma OAI.Release061.Hermitian.scalarPointSymmetryMap_fixed_iff line 143