Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-19 14:00 9801c1c0

View on Github →

feat(continued_fractions) add stabilisation under termination lemmas (#2451)

continued fractions: add lemmas for stabilisation of computations under termination and add them to default exports
seq: make argument in seq.terminated_stable explicit

Estimated changes

Modified src/algebra/continued_fractions/default.lean

Created src/algebra/continued_fractions/terminated_stable.lean

added theorem generalized_continued_fraction.continuants_aux_stable_of_terminated

added theorem generalized_continued_fraction.continuants_aux_stable_step_of_terminated

added theorem generalized_continued_fraction.continuants_stable_of_terminated

added theorem generalized_continued_fraction.convergents'_aux_stable_of_terminated

added theorem generalized_continued_fraction.convergents'_aux_stable_step_of_terminated

added theorem generalized_continued_fraction.convergents'_stable_of_terminated

added theorem generalized_continued_fraction.convergents_stable_of_terminated

added theorem generalized_continued_fraction.denominators_stable_of_terminated

added theorem generalized_continued_fraction.numerators_stable_of_terminated

added theorem generalized_continued_fraction.terminated_stable

Modified src/data/seq/seq.lean

modified theorem seq.terminated_stable