smul_algebra_smul_comm — Mathlib

English

For r∈R, a∈A, m∈M, a • r • m = r • a • m; the A-action on M commutes with the R-action on M.

Русский

Для любых r∈R, a∈A, m∈M выполняется a • r • m = r • a • m; действие A на M и действие R на M взаимно commuting.

LaTeX

$$$\\forall r\\in R\\, \\forall a\\in A\\, \\forall m\\in M:\\ a \\cdot r \\cdot m = r \\cdot a \\cdot m$$$

Lean4

theorem smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
  smul_comm _ _ _

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