self_intCast_mul

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#Commute.self_intCast_mul

English

For any a ∈ α and n ∈ ℤ, a commutes with n·a.

Русский

Для любого a ∈ α и целого n ∈ ℤ элемент a коммутирует с n·a.

LaTeX

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

Lean4

theorem self_intCast_mul : Commute a (n * a : α) :=
  (Commute.refl a).intCast_mul_right n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru