int_mul_sub_eq — Mathlib

English

If f is periodic with period c in a NonAssocRing α, then f(n·c − x) = f(−x) for all integers n and all x.

Русский

Если f периодична с периодом c в кольце без ассоциаций α, то для всех целых n и всех x выполняется f(n·c − x) = f(−x).

LaTeX

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

Lean4

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

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