iterate_eq_self — Mathlib

English

Let f be an involution with f ≠ id. Then f^[n] = f iff n is odd.

Русский

Пусть f — инволюция и f ≠ id. Тогда f^{n} = f тогда и только тогда, когда n нечётно.

LaTeX

$$$\forall f, \mathrm{Involutive}(f) \land f \neq \mathrm{id} \Rightarrow (f^[n] = f \iff \mathrm{Odd}(n)).$$$

Lean4

theorem iterate_eq_self (hf : Involutive f) (hne : f ≠ id) : f^[n] = f ↔ Odd n :=
  ⟨fun H ↦ not_even_iff_odd.1 fun hn ↦ hne <| by rwa [hf.iterate_even hn, eq_comm] at H, hf.iterate_odd⟩

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