iterate_even

Mathlib.Algebra.Ring.Parity

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

English

If f is an involution and n is even, then f^{n} = id.

Русский

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

LaTeX

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

Lean4

theorem iterate_even (hf : Involutive f) (hn : Even n) : f^[n] = id :=
  by
  obtain ⟨m, rfl⟩ := hn
  rw [← two_mul, hf.iterate_two_mul]

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

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

Разделы

Аффилиация

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