sub_int_mul_eq — Mathlib

English

If f is periodic with period c in an AddGroup α, then for every integer n, f(x − n·c) = f(x) for all x.

Русский

Если функция f имеет период c в(AddGroup) α, то для любого целого n выполняется f(x − n·c) = f(x) для всех x.

LaTeX

$$$[AddGroup\ α]\Rightarrow(\forall h:Periodic\ f\ c)(\forall n\in \mathbb{Z})\,\forall x:\alpha,\ f(x-n\cdot c)=f(x).$$$

Lean4

theorem sub_int_mul_eq [NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (x - n * c) = f x :=
  (h.int_mul n).sub_eq x

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