fract_periodic — Mathlib

English

The fractional-part function on a ring with a floor operation is periodic with period 1; i.e., fract(a + 1) = fract(a).

Русский

Дробная часть на кольце с операцией floor периодична с периодом 1, то есть fract(a + 1) = fract(a).

LaTeX

$$$\operatorname{fract}(a+1) = \operatorname{fract}(a)$$$

Lean4

theorem fract_periodic (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] :
    Function.Periodic Int.fract (1 : α) := fun a => mod_cast Int.fract_add_intCast a 1

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