cast_commute

Mathlib.Data.Rat.Cast.Defs

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

English

For any rational r ∈ ℚ, r.cast commutes with every a ∈ α: (↑r) a = a (↑r).

Русский

Для любого рационального r ∈ ℚ, отображение r в α коммутирует с любым a ∈ α: (↑r) a = a (↑r).

LaTeX

$$$ (\uparrow r) a = a (\uparrow r) $$$

Lean4

theorem cast_commute (r : ℚ) (a : α) : Commute (↑r) a := by
  simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)

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

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

Разделы

Аффилиация

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