Theorems · Definition · number theory

GenContFract.squashSeq

{K : Type u_1} → [DivisionRing K] → Stream'.Seq (GenContFract.Pair K) → ℕ → Stream'.Seq (GenContFract.Pair K)

Given a sequence of GenContFract.Pairs s = [(a₀, b₀), (a₁, b₁), ...], squashSeq s n combines ⟨aₙ, bₙ⟩ and ⟨aₙ₊₁, bₙ₊₁⟩ at position n to ⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩. For example, squashSeq s 0 = [(a₀, b₀ + a₁ / b₁), (a₁, b₁),...]. If s.TerminatedAt (n + 1), then squashSeq s n = s.

Defined in

Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Cited by

7 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRing