cast_comm

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.cast_comm

English

For all integers n and a in α, the cast of n commutes with a.

Русский

Для всех целочисленных n и элементов a в α приведение n коммутирует с a.

LaTeX

$$$ \forall (n : \mathbb{Z}) (a : \alpha), Commute (n.cast) a$$$

Lean4

theorem cast_comm (n : ℤ) (x : α) : n * x = x * n :=
  (cast_commute ..).eq

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

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

Разделы

Аффилиация

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