even_nsmul_periodic — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem even_nsmul_periodic [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Periodic f ((2 * n) • c) :=
  mul_nsmul c 2 n ▸ h.periodic.nsmul n

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