iterate_left

Mathlib.Logic.Function.Iterate

URI: https://scilib.ai/kg/mathlib#Function.Commute.iterate_left

English

If f and g commute, then f^{[n]} commutes with g for all n.

Русский

Если f и g коммутируют, то f^{[n]} коммутирует с g для любого n.

LaTeX

$$$$\forall n, \; \mathrm{Commute}(f^{[n]}, g). $$$$

Lean4

theorem iterate_left (h : Commute f g) (n : ℕ) : Commute f^[n] g :=
  (h.symm.iterate_right n).symm

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

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

Разделы

Аффилиация

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