coe_smulRight — Mathlib

English

The function smulRight f x is the map that sends c in M₁ to f(c) · x; i.e., the underlying function of smulRight is given by c ↦ f(c) · x.

Русский

Функция smulRight f x есть отображение, отправляющее c ∈ M₁ в f(c) · x; то есть базовая функция smulRight равна c ↦ f(c) · x.

LaTeX

$$smulRight f x = (λ c, f c · x)$$

Lean4

@[simp]
theorem coe_smulRight (f : M₁ →ₗ[R] S) (x : M) : (smulRight f x : M₁ → M) = fun c => f c • x :=
  rfl

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