coe_mulLeft — Mathlib

English

The map x ↦ a x is the action underlying the left translation; it is given by the same as mulLeft a.

Русский

Отображение x ↦ a x является действием левого переноса, задаваемым умножением слева на a.

LaTeX

$$$\\text{The underlying function of }\\text{mulLeft}(a)\\text{ is } x \\mapsto a x.$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mulLeft (a : G) : ⇑(Homeomorph.mulLeft a) = (a * ·) :=
  rfl

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