English
For all r ∈ R and m ∈ M, the action of algebraMap R A r on m coincides with the underlying R-action: (algebraMap R A r) • m = r • m.
Русский
Для всех r∈R и m∈M действие algebraMap R A r на m совпадает с базовым действием R: (algebraMap R A r) • m = r • m.
LaTeX
$$$(\mathrm{algebraMap}\; R\; A)\, r \;\!\cdot\; m = r \!\cdot\! m.$$$
Lean4
theorem algebra_compatible_smul (r : R) (m : M) : r • m = (algebraMap R A) r • m := by
rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]