map_fract — Mathlib

English

For a real ring R with floor and fract, and AddGroup H, if f is AddConstMapClass F R H 1 b, then f(fract(x)) = f(x) − floor(x)·b.

Русский

Пусть R — кольцо с этажированием и дробной частью, H — аддитивная группа; если f удовлетворяет AddConstMapClass, то f(fract(x)) = f(x) − ⌊x⌋·b.

LaTeX

$$$ f(\operatorname{fract}(x)) = f(x) - \lfloor x \rfloor \cdot b \quad \text{for all } x \in R. $$$

Lean4

theorem map_fract {R : Type*} [Ring R] [LinearOrder R] [FloorRing R] [AddGroup H] [FunLike F R H]
    [AddConstMapClass F R H 1 b] (f : F) (x : R) : f (Int.fract x) = f x - ⌊x⌋ • b :=
  map_sub_int' ..

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