OAI/Analysis/SymmetricDomains/SignatureRootValues.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.SignElimination.sigPos_comp_le line 40
2. lemma OAI.Release061.SignElimination.sigPos_comp_surjective line 67
3. lemma OAI.Release061.SignElimination.sigNeg_comp_surjective line 78
4. def OAI.Release061.SignElimination.signedSignature line 90
5. lemma OAI.Release061.SignElimination.signature_weightedSumSquares line 93
6. def OAI.Release061.SignElimination.squareRootOrOne line 109
7. lemma OAI.Release061.SignElimination.squareRootOrOne_sq line 112
8. lemma OAI.Release061.SignElimination.squareRootOrOne_ne_zero line 116
9. def OAI.Release061.SignElimination.rootCoordinates line 124
10. theorem OAI.Release061.SignElimination.signature_of_root_values line 154