stream_zero — Mathlib

English

Let K be a division ring with a linear order and a floor operator. The zeroth term of the stream of integer–fractional parts of v is the pair produced by taking v itself. In symbols: IntFractPair.stream v 0 = Some(IntFractPair.of v).

Русский

Пусть K — делительное кольцо, упорядоченное, с операцией floor. Нулевой член потока целочисленно-дробной части числа v равен паре, получаемой из самого v: IntFractPair.stream v 0 = Some(IntFractPair.of v).

LaTeX

$$$\operatorname{IntFractPair}.\operatorname{stream}(v,0) = \mathrm{Some}(\operatorname{IntFractPair}.\operatorname{of}(v))$$$

Lean4

theorem stream_zero (v : K) : IntFractPair.stream v 0 = some (IntFractPair.of v) :=
  rfl

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