algebra_compatible_smul — Mathlib

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]

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