const_smul₀ — Mathlib

English

If f is periodic with a positive period c in an ordered additive group, then for every x there exists y in the half-open interval [0,c) such that f(x) = f(y).

Русский

Если функция периодична с положительным периодом c в упорядоченной аддитивной группе, то для каждого x существует y в полузакрытом интервале [0, c) такой, что f(x) = f(y).

LaTeX

$$$\text{Periodic}(f,c)\land 0

Lean4

protected theorem const_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α] (h : Periodic f c) (a : γ) :
    Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x =>
  by
  by_cases ha : a = 0
  · simp only [ha, zero_smul]
  · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

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