OAI/Analysis/SymmetricDomains/RawQuadraticModelNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.residualQuadraticCoefficients line 39
2. lemma OAI.Release061.residualQuadraticCoefficients_diag line 48
3. lemma OAI.Release061.residualQuadraticCoefficients_continuous line 63
4. lemma OAI.Release061.residualQuadraticCoefficients_zero line 73
5. def OAI.Release061.Biholomorph.ofEntireHomeomorph line 80
6. theorem OAI.Release061.quadraticShear_biholomorph line 86
7. theorem OAI.Release061.raw_quadratic_model_normalization line 126