instNSMul — Mathlib

English

There is a natural-number scalar action on R[X] defined via lifting scalars to coefficients, i.e., r • p corresponds to multiplying all coefficients by r.

Русский

Существет действие натурального числа на R[X], где умножение каждого коэффициента полинома на r → r • p.

LaTeX

$$$ \text{instNSMul} : \mathrm{SMul}\ \mathbb{N}\ R[X] $$$

Lean4

instance instNSMul : SMul ℕ R[X] where smul r p := ⟨r • p.toFinsupp⟩

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