mul_const' — Mathlib

English

If f is antiperiodic with c, then for 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)$ 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) := by simpa only [div_eq_mul_inv] using h.mul_const ha

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