const_inv_smul — Mathlib

English

If f is antiperiodic with c, then for any scalar a, the function x ↦ f(a⁻¹·x) is antiperiodic with period a·c.

Русский

Если f антипериодическая с c, то для любого скаляра a функция x ↦ f(a⁻¹·x) антипериодична с периодом a·c.

LaTeX

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

Lean4

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

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