smul_eq_C_mul — Mathlib

English

For every r ∈ K and x ∈ RatFunc K, the scalar action of r on x coincides with multiplication by the constant C r: r • x = C r · x.

Русский

Для любого r ∈ K и x ∈ RatFunc K скалярное умножение на r совпадает с умножением на константу C r: r • x = C r · x.

LaTeX

$$$ r \cdot x = C r \cdot x $$$

Lean4

theorem smul_eq_C_mul (r : K) (x : RatFunc K) : r • x = C r * x := by rw [Algebra.smul_def, algebraMap_eq_C]

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