cast_comm

Mathlib.Data.Rat.Cast.Defs

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

English

A nonnegative rational q commutes with every a ∈ α: q a = a q in α.

Русский

Неотрицательное рациональное число q коммутирует с любым a ∈ α: q a = a q в α.

LaTeX

$$$ (\uparrow q) a = a (\uparrow q) $$$

Lean4

theorem cast_comm (q : ℚ≥0) (a : α) : q * a = a * q :=
  cast_commute _ _

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

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

Разделы

Аффилиация

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