coe_mulRight — Mathlib

English

The underlying function of the right multiplication map coincides with the expected pointwise map y ↦ yx.

Русский

Базовая функция карты правого умножения совпадает с ожидаемой точечно-заданной картой y ↦ yx.

LaTeX

$$$\\operatorname{coe}(\\text{ContinuousMap.mulRight } x) = (\\lambda y. yx)$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_mulRight (x : X) : ⇑(ContinuousMap.mulRight x) = fun y => y * x :=
  rfl

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