sameCycle_pow_right — Mathlib

English

Replacing y by (f^n) y preserves SameCycle: SameCycle f x ((f^n) y) ↔ SameCycle f x y for n ∈ ℕ.

Русский

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

LaTeX

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

Lean4

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

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