smul_def — Mathlib

English

The scalar action of a polynomial f ∈ R[X] on an element m ∈ PolynomialModule R M is given by evaluating f at the endomorphism (Finsupp.lmapDomain M R Nat.succ) applied to m.

Русский

Действие скаляра полинома f ∈ R[X] на элемент m ∈ PolynomialModule R M задаётся вычислением f в концеоморфизме (Finsupp.lmapDomain M R Nat.succ) применительно к m.

LaTeX

$$$f \cdot m = \mathrm{aeval}_{\mathrm{Finsupp.lmapDomain\ M\ R\ Nat.succ}}(f)(m)$$$

Lean4

theorem smul_def (f : R[X]) (m : PolynomialModule R M) : f • m = aeval (Finsupp.lmapDomain M R Nat.succ) f m := by rfl

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