algebraMap_apply — Mathlib

English

For k ∈ R and a ∈ α, the value of algebraMap R C(α,A) at k, evaluated at a, equals k • 1_A.

Русский

Для k ∈ R и a ∈ α значение algebraMap R C(α,A) на k, применённое к a, равно k • 1_A.

LaTeX

$$$\\operatorname{algebraMap}_{{R}}^{C(\\alpha,A)}(k)(a) = k \\cdot 1_A.$$$

Lean4

@[simp]
theorem algebraMap_apply (k : R) (a : α) : algebraMap R C(α, A) k a = k • (1 : A) :=
  by
  rw [Algebra.algebraMap_eq_smul_one]
  rfl

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