mul_const' — Mathlib

English

If f is periodic with period c, then f(x) with a scaled argument has period c/a.

Русский

Если f периодична с периодом c, то для аргумента, масштабированного на a, период становится c/a.

LaTeX

$$$\text{Periodic}(f,c)\Rightarrow \forall a, \text{Periodic}(\lambda x. f(x\cdot a), c/a)$$$

Lean4

theorem mul_const' [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun x => f (x * a)) (c / a) := by
  simpa only [div_eq_mul_inv] using h.mul_const a

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