iterate_odd

Mathlib.Algebra.Ring.Parity

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem iterate_odd (hf : Involutive f) (hn : Odd n) : f^[n] = f :=
  by
  obtain ⟨m, rfl⟩ := hn
  rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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