algebraMap_eq_smul_one — Mathlib

English

For any r ∈ R, the image algebraMap R A r equals r acting on the unit: algebraMap R A r = r • 1.

Русский

Для любого r ∈ R образ algebraMap R A r равен действию скаляра на единицу: algebraMap R A r = r • 1.

LaTeX

$$$\operatorname{algebraMap}(R,A)(r) = r \cdot 1_A$$$

Lean4

theorem algebraMap_eq_smul_one (r : R) : algebraMap R A r = r • (1 : A) :=
  calc
    algebraMap R A r = algebraMap R A r * 1 := (mul_one _).symm
    _ = r • (1 : A) := (Algebra.smul_def r 1).symm

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