OAI/Algebra/Divisor/RationalRecovery.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ControlledBoundary.RationalRecovery.Form line 16
2. def OAI.ControlledBoundary.RationalRecovery.Form.eval line 25
3. def OAI.ControlledBoundary.RationalRecovery.Form.tail line 29
4. def OAI.ControlledBoundary.RationalRecovery.Form.combine line 33
5. lemma OAI.ControlledBoundary.RationalRecovery.Form.eval_combine line 36
6. lemma OAI.ControlledBoundary.RationalRecovery.Form.eval_succ line 43
7. lemma OAI.ControlledBoundary.RationalRecovery.Form.cast_eval line 48
8. lemma OAI.ControlledBoundary.RationalRecovery.finite_interval line 56
9. lemma OAI.ControlledBoundary.RationalRecovery.finite_interval_indexed line 69
10. theorem OAI.ControlledBoundary.RationalRecovery.exists_rat_solution line 84
11. def OAI.ControlledBoundary.RationalRecovery.realify line 163
12. lemma OAI.ControlledBoundary.RationalRecovery.realify_apply line 166
13. theorem OAI.ControlledBoundary.RationalRecovery.recover_coefficients line 171
14. theorem OAI.ControlledBoundary.RationalRecovery.rational_recovery line 203