const_mul

Mathlib.Algebra.Field.Periodic

URI: https://scilib.ai/kg/mathlib#Function.Periodic.const_mul

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru