mul_coe_eq_smul

Mathlib.Algebra.Quaternion

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

English

Multiplication by a scalar on the right coincides with the scalar action: a · ↑r = r • a.

Русский

Умножение на скаляр справа равно скалярному действию: a · ↑r = r • a.

LaTeX

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

Lean4

theorem mul_coe_eq_smul : a * r = r • a := by rw [← coe_commutes, coe_mul_eq_smul]

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

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

Разделы

Аффилиация

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