OAI/Analysis/SymmetricDomains/QuadraticModelResidualFiber.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.Hermitian.normalTranslation line 36
  2. lemma OAI.Release061.Hermitian.normalTranslation_analytic line 40
  3. lemma OAI.Release061.Hermitian.normalTranslation_mem line 46
  4. def OAI.Release061.Hermitian.axisNormalization line 55
  5. lemma OAI.Release061.Hermitian.axisNormalization_apply line 60
  6. lemma OAI.Release061.Hermitian.axisNormalization_mem line 71
  7. lemma OAI.Release061.Hermitian.axisNormalization_analytic line 79
  8. def OAI.Release061.Hermitian.axisNormalizationModel line 86
  9. lemma OAI.Release061.Hermitian.axisNormalization_inverse_analytic line 91
  10. theorem OAI.Release061.Hermitian.quadratic_model_residual_fiber_transitive line 101