even_zsmul_periodic — Mathlib

English

For AddGroup α and InvolutiveNeg β, if f is antiperiodic with c, then f is periodic with period (2·n)·c for any integer n.

Русский

Для AddGroup α и InvolutiveNeg β, если f антипериодична с c, то она периодична с периодом (2n)·c для любого целого n.

LaTeX

$$$[AddGroup\ α][InvolutiveNeg\ β]\Rightarrow(\forall h:Antiperiodic\ f\ c)(\forall n\in \mathbb{Z})\, Periodic\ f\ ((2\cdot n)\cdot c).$$$

Lean4

theorem even_zsmul_periodic [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Periodic f ((2 * n) • c) :=
  by
  rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]
  exact h.periodic.zsmul n

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