mul_def — Mathlib

English

The explicit multiplication rule for the regular wreath product: (d,f)(d',f') = ( d · ( f · d'), f f' ), with (f · d')(x) = d'(f^{-1}x).

Русский

Явное правило умножения в регулярном wreath-продукте: (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

theorem mul_def (a b : D ≀ᵣ Q) : a * b = ⟨a.1 * fun x ↦ b.1 (a.2⁻¹ * x), a.2 * b.2⟩ :=
  rfl

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