intCast_mul_left — Mathlib

English

If a and b commute in a ring α, then for every integer m, (m·a) commutes with b.

Русский

Если a и b коммутируют в кольце α, то для каждого целого m выполняется, что (m·a) коммутирует с b.

LaTeX

$$$$ \\forall a,b \\in \\alpha,\\ Commute a b \\Rightarrow \\forall m \\in \\mathbb{Z}, \\ Commute (m \\cdot a) b. $$$$

Lean4

theorem intCast_mul_left (h : Commute a b) (m : ℤ) : Commute (m * a) b := by simp [h]

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