coe_mul_eq_smul

Mathlib.Algebra.Quaternion

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

English

Multiplication by the embedded scalar on the left equals scalar multiplication of the quaternion.

Русский

Умножение слева на встроенный скаляр равно скалярному умножению кватерниона.

LaTeX

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

Lean4

theorem coe_mul_eq_smul : ↑r * a = r • a :=
  QuaternionAlgebra.coe_mul_eq_smul r a

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

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

Разделы

Аффилиация

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