sub_zsmul_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 в группе с операцией сложения; тогда для любого целого числа 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_zsmul_eq [AddGroup α] (h : Periodic f c) (n : ℤ) : f (x - n • c) = f x :=
  (h.zsmul n).sub_eq x

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