mul_coe_eq_smul

Mathlib.Algebra.Quaternion

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

English

Multiplication by a scalar on the right corresponds to scalar multiplication.

Русский

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

LaTeX

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

Lean4

theorem mul_coe_eq_smul : a * r = r • a :=
  QuaternionAlgebra.mul_coe_eq_smul r a

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

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

Разделы

Аффилиация

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