coe_commute

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.coe_commute

English

The coercion of R into ℍ[R] commutes with multiplication by any quaternion element.

Русский

Встраивание скаляра в ℍ[R] commute с умножением на элементы кватерниона.

LaTeX

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

Lean4

theorem coe_commute : Commute (↑r) a :=
  QuaternionAlgebra.coe_commute r a

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

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

Разделы

Аффилиация

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