Commit 2020-05-27 12:11 2deb6b46
View on Github →feat(algebra/continued_fractions): add computation definitions and basic translation lemmas (#2797)
What
- add definitions of the computation of a continued fraction for a given value (in a given floor field)
- add very basic, mostly technical lemmas to convert between the different structures used by the computation
Why
- I want to be able to compute the continued fraction of a value. I next will add termination, approximation, and correctness lemmas for the definitions in this commit (I already have them lying around on my PC for ages :cold_sweat: )
- The technical lemmas are needed for the next bunch of commits.
How
- Follow the straightforward approach as described, for example, on Wikipedia