OAI/Analysis/SymmetricDomains/ScalarTubeInvolution.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.scalarTube line 36
  2. def OAI.Release061.scalarNormalInversion line 38
  3. lemma OAI.Release061.scalarTube_im_pos line 42
  4. lemma OAI.Release061.scalarTube_normal_ne_zero line 46
  5. lemma OAI.Release061.scalarNormalInversion_residual line 52
  6. lemma OAI.Release061.scalarNormalInversion_mem line 63
  7. lemma OAI.Release061.scalarNormalInversion_involutive line 72
  8. lemma OAI.Release061.scalarNormalInversion_axis line 88
  9. lemma OAI.Release061.scalarNormalInversion_analytic line 97
  10. lemma OAI.Release061.scalarNormalInversion_fixed_iff line 105
  11. def OAI.Release061.scalarTubeInvolution line 139