instMul

Mathlib.Algebra.Group.End

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

English

The product of two permutations is their composition: f * g = g ∘ f.

Русский

Произведение двух перестановок есть их композиция: f * g = g ∘ f.

LaTeX

$$$\\\\forall f,g \\\\in \\\\operatorname{Perm}(\\\\alpha), \\\\ f * g = g \\\\\\text{trans} f$$$

Lean4

instance instMul : Mul (Perm α) where mul f g := Equiv.trans g f

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

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

Разделы

Аффилиация

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