coe_mul_eq_smul — Mathlib

English

Multiplication by a scalar inside the base ring corresponds to scalar action inside QuadraticAlgebra.

Русский

Умножение на скаляр внутри основания кольца соответствует действию скаляра внутри QuadraticAlgebra.

LaTeX

$$$\operatorname{coe}(r) \; *\; x = r \; \cdot\; x$ in QuadraticAlgebra$$

Lean4

theorem coe_mul_eq_smul (r : R) (x : QuadraticAlgebra R a b) : (r * x : QuadraticAlgebra R a b) = r • x := by
  ext <;> simp

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