instPowNat

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.instPowNat

English

The powers of a permutation are defined by iteration: f^n = f^[n].

Русский

Степени перестановки определяются итерацией: f^n = f^[n].

LaTeX

$$$\\\\forall f \\\\in \\\\operatorname{Perm}(\\\\alpha), \\\\forall n \\\\in \\\\mathbb{N}, \\\\ f^{n} = f^[n]$$$

Lean4

instance instPowNat : Pow (Perm α) ℕ where pow f n := ⟨f^[n], f.symm^[n], f.left_inv.iterate _, f.right_inv.iterate _⟩

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

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

Разделы

Аффилиация

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