algebraMap_apply — Mathlib

English

The action of the base field 𝕜 on the bounded function space is given by constant functions via algebraMap, i.e., algebraMap 𝕜 (α →ᵇ γ) k acts as k times the unit function.

Русский

Действие базового поля 𝕜 на пространстве ограниченных функций задаётся через константные функции: algebraMap 𝕜 (α →ᵇ γ) k действует как k умноженное на единичную функцию.

LaTeX

$$$algebraMap 𝕜 (α \\to^b γ) \\, k \\, a = k \\cdot 1_{γ}$$$

Lean4

@[simp]
theorem algebraMap_apply (k : 𝕜) (a : α) : algebraMap 𝕜 (α →ᵇ γ) k a = k • (1 : γ) := by
  simp only [Algebra.algebraMap_eq_smul_one, coe_smul, coe_one, Pi.one_apply]

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