OAI/Analysis/SymmetricDomains/ScalarConeImagePositive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.Hermitian.bilinearNormalCoordinates line 38
2. lemma OAI.Release061.Hermitian.hermQuadratic_half_sum line 59
3. lemma OAI.Release061.Hermitian.hermQuadratic_bilinearNormalCoordinates line 69
4. lemma OAI.Release061.Hermitian.supportLinearCoordinates_hermitian_residual line 77
5. lemma OAI.Release061.Hermitian.supportLinearCoordinates_hermitian_mem line 91
6. lemma OAI.Release061.Hermitian.scalar_cone_image_eq_positive line 104