iterate_eq_id — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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