of — Mathlib · SciLib

English

The construction of SimpContFract.of v yields a SimpContFract, i.e., the resulting object satisfies the simple continued fraction axioms.

Русский

Конструкция SimpContFract.of v удовлетворяет свойствам простого продолженного дробления.

LaTeX

$$$\\\\forall {K} (v : K) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K], (SimpContFract.of v).IsSimpContFract$$$

Lean4

/-- Creates the simple continued fraction of a value. -/
def of : SimpContFract K :=
  ⟨GenContFract.of v, GenContFract.of_isSimpContFract v⟩

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