instInv

Mathlib.GroupTheory.RegularWreathProduct

URI: https://scilib.ai/kg/mathlib#RegularWreathProduct.instInv

English

The inverse in the wreath product is given by inv(d,f) = (x ↦ d(x)^{-1} (f^{-1}⋅x), f^{-1}).

Русский

Обратный элемент в wreath-продукте имеет вид inv(d,f) = (x ↦ d(x)^{-1} (f^{-1}⋅x), f^{-1}).

LaTeX

$$$\operatorname{inv}(d,f) = \big( x \mapsto d(x)^{-1} \cdot (f^{-1}x),\ f^{-1} \big).$$$

Lean4

instance : Inv (RegularWreathProduct D Q) where inv x := ⟨fun k ↦ x.1⁻¹ (x.2 * k), x.2⁻¹⟩

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

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

Разделы

Аффилиация

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