cast_comm

Mathlib.Data.Nat.Cast.Commute

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

English

For any α with a NonAssocSemiring structure, (n : α) * x = x * (n : α).

Русский

Для любого α с неассоциативной структурой, (n : α) умножается слева и справа на x одинаково.

LaTeX

$$$$ (n : \alpha) \cdot x = x \cdot (n : \alpha) $$$$

Lean4

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

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

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

Разделы

Аффилиация

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