Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-08 19:42 3e5d90d9

View on Github →

feat(algebra/continued_fractions) add determinant formula and approximations for error term (#6461)

Estimated changes

Modified src/algebra/continued_fractions/basic.lean

Modified src/algebra/continued_fractions/computation/approximations.lean

added theorem generalized_continued_fraction.abs_sub_convergents_le'

added theorem generalized_continued_fraction.abs_sub_convergents_le

added theorem generalized_continued_fraction.determinant

added theorem generalized_continued_fraction.determinant_aux

added theorem generalized_continued_fraction.sub_convergents_eq

Modified src/algebra/continued_fractions/computation/correctness_terminating.lean

Modified src/algebra/continued_fractions/computation/terminates_iff_rat.lean