intCast_right — Mathlib

English

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

Русский

Пусть α — кольцо без ассоциативности. Тогда для любого a ∈ α и любого n ∈ ℤ элемент n помещённый в α коммутирует с a.

LaTeX

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

Lean4

@[simp]
theorem intCast_right : Commute a n :=
  Int.commute_cast _ _

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