instMul — Mathlib

English

In the regular wreath product D ≀ᵣ Q, the product of two elements (d,f) and (d',f') is given by (d,f)(d',f') = ( d · ( f · d'), f f'), where (f · d')(x) = d'( f^{-1} x ).

Русский

В регулярном wreath-продукте D ≀ᵣ Q произведение двух элементов (d,f) и (d',f') задаётся как (d,f)(d',f') = ( d · ( f · d'), f f'), где (f · d')(x) = d'( f^{-1} x ).

LaTeX

$$$\big( d,f \big) \cdot \big( d',f' \big) = \Big( d \cdot ( f \cdot d'), \; f f' \Big), \quad (f \cdot d')(x) = d'(f^{-1}x).$$$

Lean4

instance : Mul (D ≀ᵣ Q) where mul a b := ⟨a.1 * (fun x ↦ b.1 (a.2⁻¹ * x)), a.2 * b.2⟩

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