div_inv — 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 / a), c a)$ for all $a \neq 0$$$

Lean4

theorem div_inv [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_inv ha

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