const_smul₀ — Mathlib

English

If f is antiperiodic with period c, then for any nonzero a the function x ↦ f(a x) is antiperiodic with period a^{-1} c.

Русский

Если f антипериодична с периодом c, то для любого не нулевого a функция x ↦ f(a x) антипериодична с периодом a^{-1} c.

LaTeX

$$$\text{Antiperiodic}(f\circ (a\cdot), a^{-1} c)$ for all $a \neq 0$$$

Lean4

theorem const_smul₀ [AddMonoid α] [Neg β] [GroupWithZero γ] [DistribMulAction γ α] (h : Antiperiodic f c) {a : γ}
    (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
  simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

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