ergodic_nsmul

Mathlib.Dynamics.Ergodic.AddCircle

URI: https://scilib.ai/kg/mathlib#AddCircle.ergodic_nsmul

English

Ergodicity for n times the action on the circle for n > 1 in natural numbers.

Русский

Эргодичность для n-кратного действия на окружности, где n > 1.

LaTeX

$$$\forall n:\mathbb{N}, n>1 \Rightarrow Ergodic (n \cdot)\text{ on circle}$$$

Lean4

theorem ergodic_nsmul {n : ℕ} (hn : 1 < n) : Ergodic fun y : AddCircle T => n • y :=
  ergodic_zsmul (by simp [hn] : 1 < |(n : ℤ)|)

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

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

Разделы

Аффилиация

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