smul_coe

Mathlib.Algebra.QuadraticAlgebra

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

English

r1 • (r2 : QuadraticAlgebra R a b) = ↑(r1 * r2).

Русский

r1 на (r2), где r2 ∈ QuadraticAlgebra, равняется ⟨r1 r2⟩.

LaTeX

$$$r_1 \; \smul\; (r_2 : \QuadraticAlgebra R a b) = ↑(r_1 r_2)$$$

Lean4

theorem smul_coe (r1 r2 : R) : r1 • (r2 : QuadraticAlgebra R a b) = ↑(r1 * r2) := by rw [coe_mul, coe_mul_eq_smul]

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

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

Разделы

Аффилиация

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