const_smul — Mathlib

English

If f is antiperiodic with c and a is a scalar, then the scaled function a•f is antiperiodic with period a⁻¹•c.

Русский

Если f антипериодическая с c и a — скаляр, то функция a•f антипериодична с периодом a⁻¹•c.

LaTeX

$$$\text{Antiperiodic}(f,c) \rightarrow \text{Antiperiodic}(a\cdot f, a^{-1}\cdot c)$$$

Lean4

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

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