intCast_left — Mathlib

English

Let α be a (not necessarily associative) ring and a ∈ α. Then for every integer n ∈ ℤ, the image of n in α commutes with a.

Русский

Пусть α — кольцо (без ассоциативности). Для любого a ∈ α и любого целого n ∈ ℤ образ целого числа n в α через естественное вложение коммутирует с a.

LaTeX

$$$$ \\forall a \\in \\alpha, \\forall n \\in \\mathbb{Z}, (n : \\alpha) \\cdot a = a \\cdot (n : \\alpha). $$$$

Lean4

@[simp]
theorem intCast_left : Commute (n : α) a :=
  Int.cast_commute _ _

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