mul_coe_eq_smul

Mathlib.Algebra.QuadraticAlgebra

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

English

Right multiplication by r equals scalar multiplication by r on QuadraticAlgebra R a b.

Русский

Правое умножение на r равно скалярному умножению на r на QuadraticAlgebra R a b.

LaTeX

$$$(x \cdot r) = (r \cdot x) \\text{ in }(\QuadraticAlgebra R a b)$$$

Lean4

theorem mul_coe_eq_smul (r : R) (x : QuadraticAlgebra R a b) : (x * r : QuadraticAlgebra R a b) = r • x := by
  rw [mul_comm, coe_mul_eq_smul r x]

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

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

Разделы

Аффилиация

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