OAI/Analysis/SymmetricDomains/HolQuadraticSmul.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Hermitian.holQuadratic line 36
  2. def OAI.Release061.Hermitian.hermQuadratic line 39
  3. lemma OAI.Release061.Hermitian.vector_decomposition line 43
  4. lemma OAI.Release061.Hermitian.holQuadratic_analytic line 48
  5. lemma OAI.Release061.Hermitian.holQuadratic_continuous line 52
  6. def OAI.Release061.Hermitian.quadraticShear line 56
  7. lemma OAI.Release061.Hermitian.quadraticShear_analytic line 67
  8. lemma OAI.Release061.Hermitian.quadraticShear_inverse_analytic line 72
  9. lemma OAI.Release061.Hermitian.quadraticShear_residual line 77
  10. theorem OAI.Release061.Hermitian.quadraticShear_preimage line 87
  11. lemma OAI.Release061.Hermitian.hermQuadratic_unit line 95
  12. lemma OAI.Release061.Hermitian.hermQuadratic_real_smul line 101
  13. lemma OAI.Release061.Hermitian.holQuadratic_smul line 109