const_inv_mul — Mathlib

English

If f is periodic with period c, then f(a⁻¹·x) is periodic with period a·c.

Русский

Если f периодична с периодом c, то f(a⁻¹·x) периодична с периодом a·c.

LaTeX

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

Lean4

theorem const_inv_mul [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun x => f (a⁻¹ * x)) (a * c) :=
  h.const_inv_smul₀ a

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