const_inv_smul₀ — Mathlib

English

If f is antiperiodic with c, then for nonzero 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(a^{-1}\cdot), a c)$ for all $a \neq 0$$$

Lean4

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

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