single — Mathlib

English

The PolynomialModule defines a module-valued type with finsupp structure over M.

Русский

PolynomialModule задаёт модуль-тип с структурой Finsupp над M.

LaTeX

$$$PolynomialModule\; R\; M := \mathbb{N} \to_0 M$$$

Lean4

/-- The monomial `m * x ^ i`. This is defeq to `Finsupp.singleAddHom`, and is redefined here
so that it has the desired type signature. -/
noncomputable def single (i : ℕ) : M →+ PolynomialModule R M :=
  Finsupp.singleAddHom i

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