Theorems · Definition · number theory

GenContFract.nextConts

{K : Type u_2} → [DivisionRing K] → K → K → GenContFract.Pair K → GenContFract.Pair K → GenContFract.Pair K

Returns the next continuants ⟨Aₙ, Bₙ⟩ using nextNum and nextDen, where pred is ⟨Aₙ₋₁, Bₙ₋₁⟩, ppred is ⟨Aₙ₋₂, Bₙ₋₂⟩, a is aₙ₋₁, and b is bₙ₋₁.

Defined in

Mathlib.Algebra.ContinuedFractions.Basic

Cited by

9 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Quot.sound

Assumes

DivisionRing