commute_cast

Mathlib.Data.Rat.Cast.Defs

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

English

Let a be in a division ring α and r ∈ ℚ. Then a and r cast to α commute: a · (r : α) = (r : α) · a.

Русский

Пусть a ∈ α и r ∈ ℚ. Тогда a и (r) в α коммутируют: a · (r : α) = (r : α) · a.

LaTeX

$$$\forall a \in \alpha, \forall r \in \mathbb{Q}, \ a \cdot (r : \alpha) = (r : \alpha) \cdot a.$$$

Lean4

theorem commute_cast (a : α) (r : ℚ) : Commute a r :=
  (r.cast_commute a).symm

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

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

Разделы

Аффилиация

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