const_mul

Mathlib.Dynamics.PeriodicPts.Defs

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

English

If f x = f y with x, y periodic with periods m, n (both positive), then x = y.

Русский

Если f(x) = f(y) и x, y периодичны с периодами m, n (оба положительные), то x = y.

LaTeX

$$$IsPeriodicPt f m x \to IsPeriodicPt f n y \to 0 < m \to 0 < n \to f x = f y \Rightarrow x = y$$$

Lean4

protected theorem const_mul (hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (n * m) x := by
  simp only [mul_comm n, hm.mul_const n]

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

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

Разделы

Аффилиация

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