of_h_eq_intFractPair_seq1_fst_b — Mathlib

English

The head term of the generalized continued fraction of v is the pair whose first component is 1 and whose second component is floor of the inverse of the fractional part of v.

Русский

Головной член непрерывной цепной дроби числа v имеет форму пары (1, floor(frac(v)^{-1})).

LaTeX

$$$\operatorname{(of\,v)}.s.head = \mathrm{Some}(\langle 1, \lfloor(\operatorname{fract} v)^{-1} \rfloor\rangle)$$$

Lean4

theorem of_h_eq_intFractPair_seq1_fst_b : (of v).h = (IntFractPair.seq1 v).fst.b :=
  by
  cases aux_seq_eq : IntFractPair.seq1 v
  simp [of, aux_seq_eq]

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