mul_left — Mathlib

English

In the regular wreath product, the left component of the product equals a.1 · (b.1 applied pointwise by a.2).

Русский

В регулярном wreath-продукте левая компонента произведения равна a.1 · (б.1, применяемого по точкам согласно a.2).

LaTeX

$$$\big( a \cdot b \big).1 = a.1 \cdot \big( x \mapsto b.1\big( a.2^{-1} \cdot x \big) \big).$$$

Lean4

@[simp]
theorem mul_left (a b : D ≀ᵣ Q) : (a * b).1 = a.1 * fun x ↦ b.1 (a.2⁻¹ * x) :=
  rfl

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