mul_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_const [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) :
    Antiperiodic (fun x => f (x * a)) (c * a⁻¹) :=
  h.const_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha

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