X — Mathlib · SciLib

English

For each s, X_s is the monomial corresponding to the exponent with 1 in the s-th coordinate and coefficient 1.

Русский

Для каждой переменной s в многомерном формальном ряде X_s является мономом с единичным коэффициентом в координате s и нулевыми во всех остальных.

LaTeX

$$$X_s = \mathrm{monomial}(\mathrm{single}(s,1), 1)$$$

Lean4

/-- The variables of the multivariate formal power series ring. -/
def X (s : σ) : MvPowerSeries σ R :=
  monomial (single s 1) 1

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