smulRightL_apply — Mathlib

English

For a scalar-valued continuous multilinear map f on E, the right action by z ∈ G via the operation smulRightL coincides with the standard right action on the outputs: smulRightL 𝕜 E G f z = f.smulRight z.

Русский

Для скалярно-значимой непрерывной многолинией отображения f на E операция правого умножения на вектор z∈G через smulRightL совпадает с обычной операцией правого умножения на z: smulRightL 𝕜 E G f z = f.smulRight z.

LaTeX

$$$ smulRightL_{\mathbb{k}} E G f z = f.smulRight z $$$

Lean4

@[simp]
theorem smulRightL_apply (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) : smulRightL 𝕜 E G f z = f.smulRight z :=
  rfl

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