intCast_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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