sameCycle_pow_left — Mathlib

English

Replacing x by (f^n) x for n a natural number preserves SameCycle: SameCycle f ((f^n) x) y ↔ SameCycle f x y.

Русский

Замена x на (f^n) x для натурального n сохраняет SameCycle: SameCycle f ((f^n) x) y ↔ SameCycle f x y.

LaTeX

$$$\\forall n\\in\\mathbb{N},\\; SameCycle\\ f\\ ((f^n) x)\\ y \\iff SameCycle\\ f\\ x\\ y.$$$

Lean4

@[simp]
theorem sameCycle_pow_left {n : ℕ} : SameCycle f ((f ^ n) x) y ↔ SameCycle f x y := by
  rw [← zpow_natCast, sameCycle_zpow_left]

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