smul_left — Mathlib

English

If a and b commute, then r • a commutes with b for any r in M.

Русский

Если a и b commute, то r • a commute с b для любого r ∈ M.

LaTeX

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

Lean4

@[to_additive]
theorem smul_left [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α} (h : Commute a b) (r : M) :
    Commute (r • a) b :=
  (h.symm.smul_right r).symm

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