smul_right — Mathlib

English

If a and b commute and one has a scalar action by M, then a commutes with r • b for any r ∈ M.

Русский

Если a и b commute и есть скалярное действие M, то a commuting с r•b для любого r ∈ M.

LaTeX

$$$\\\\forall a,b \\\\in \\\\alpha, \\\\Commute a b \\\\rightarrow \\\\forall r \\\\in M, \\\\ Commute a (r \\\\cdot b).$$$

Lean4

@[to_additive]
theorem smul_right [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α} (h : Commute a b) (r : M) :
    Commute a (r • b) :=
  (mul_smul_comm _ _ _).trans ((congr_arg _ h).trans <| (smul_mul_assoc _ _ _).symm)

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