translationNumber_zpow

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.translationNumber_zpow

← MathLib Explorer

English

For f ∈ CircleDeg1Liftˣ and integer n, τ(f^n) = n · τ(f).

Русский

Для f ∈ CircleDeg1Liftˣ и целого n, τ(f^n) = n · τ(f).

LaTeX

$$$ \forall f \in CircleDeg1Lift^{\times}, \forall n \in \mathbb{Z}, \ τ(f^{n}) = n \cdot τ(f). $$$

Lean4

@[simp]
theorem translationNumber_zpow (f : CircleDeg1Liftˣ) : ∀ n : ℤ, τ (f ^ n : Units _) = n * τ f
  | (n : ℕ) => by simp [translationNumber_pow f n]
  | -[n+1] => by simp; ring

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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