OAI/Analysis/MatrixSigning/Arithmetic/RationalMagnitudeSign.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W30.RationalMagnitudeMachine.sign_initial line 10
2. theorem OAI.KS.W30.RationalMagnitudeMachine.one_initial line 11
3. lemma OAI.KS.W30.RationalMagnitudeMachine.sign_zero_first line 13
4. lemma OAI.KS.W30.RationalMagnitudeMachine.sign_zero_second line 22
5. lemma OAI.KS.W30.RationalMagnitudeMachine.sign_nonzero line 31
6. theorem OAI.KS.W30.RationalMagnitudeMachine.normalizeSign_spec line 40
7. theorem OAI.KS.W30.RationalMagnitudeMachine.zeroNumerator_spec line 66
8. theorem OAI.KS.W30.RationalMagnitudeMachine.insertOne_layout line 79
9. theorem OAI.KS.W30.RationalMagnitudeMachine.insertOne_spec line 84
10. theorem OAI.KS.W30.RationalMagnitudeMachine.zeroBranch_spec line 103
11. theorem OAI.KS.W30.RationalMagnitudeMachine.clearGCD_spec line 109