iterate_two_mul

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Function.Involutive.iterate_two_mul

English

If f is an involution, then the even iterate equals id: f^[2n] = id.

Русский

Если f — инволюция, то f^{2n} = id.

LaTeX

$$$\forall f: X \to X,\, \mathrm{Involutive}(f) \Rightarrow \forall n \in \mathbb{N},\, f^[2n] = \mathrm{id}.$$$

Lean4

theorem iterate_two_mul (hf : Involutive f) (n : ℕ) : f^[2 * n] = id := by
  rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]

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

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

Разделы

Аффилиация

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