commute_cast

Mathlib.Data.Int.Cast.Lemmas

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

English

The cast of integers commutes with any element of α; i.e., the integer image and α commute.

Русский

Образ целого числа через приведение коммутирует с любым элементом α.

LaTeX

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

Lean4

theorem commute_cast (a : α) (n : ℤ) : Commute a n :=
  (cast_commute ..).symm

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

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

Разделы

Аффилиация

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