of_isSimpContFract — Mathlib

English

The simple continued fraction of v is defined as the pair consisting of GenContFract.of v and the fact that it is a SimpContFract.

Русский

Простое непрерывное дробление числа v задаётся как пара: GenContFract.of v вместе со свойством, что она является SimpContFract.

LaTeX

$$$\\\\text{SimpContFract.of}(v) = \\\\langle GenContFract.of(v), GenContFract.of_isSimpContFract(v) \\\\rangle$$$

Lean4

theorem of_isSimpContFract : (of v).IsSimpContFract := fun _ _ nth_partNum_eq => of_partNum_eq_one nth_partNum_eq

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