intCast_mul_self

Mathlib.Data.Int.Cast.Lemmas

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

English

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

Русский

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

LaTeX

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

Lean4

theorem intCast_mul_self : Commute ((n : α) * a) a :=
  (Commute.refl a).intCast_mul_left n

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

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

Разделы

Аффилиация

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