of_s_tail — Mathlib

English

If a is an integer, the s-sequence of its of is nil.

Русский

Если a целое, s-последовательность для of a пуста.

LaTeX

$$$\operatorname GenContFract.of a.cast).s = \mathrm{Stream'.Seq.nil}$$$

Lean4

/-- This expresses the tail of the coefficient sequence of the `GenContFract.of` an element `v` of
`K` as the coefficient sequence of that of the inverse of the fractional part of `v`.
-/
theorem of_s_tail : (of v).s.tail = (of (fract v)⁻¹).s :=
  Stream'.Seq.ext fun n => Stream'.Seq.get?_tail (of v).s n ▸ of_s_succ v n

Похожие утверждения