smul_coe

Mathlib.Algebra.Quaternion

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

English

For all x and y in R, x • (y as quaternion) equals the quaternion corresponding to the product x y.

Русский

Для всех x, y в R выполняется x • (y как кватернион) = (xy) как кватернион.

LaTeX

$$$ x \\cdot (y : \\mathbb{H}(R)) = (x \\cdot y) \\text{(as quaternion)}$$$

Lean4

theorem smul_coe : x • (y : ℍ[R]) = ↑(x * y) :=
  QuaternionAlgebra.smul_coe x y

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

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

Разделы

Аффилиация

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