monomial' — Mathlib

English

A variant of HasSubst.monomial: for nonzero exponent n, the monomial with coefficient s defines a substitution of power series.

Русский

Вариант HasSubst.monomial: при ненулевом показателе n мономиал с коэффициентом s задаёт замену в рядовых степенных рядах.

LaTeX

$$$ \text{monomial}'(n, s) \text{ is a HasSubst for } n \neq 0. $$$

Lean4

/-- A variant of `HasSubst.monomial` to avoid the expansion of `Unit`. -/
protected theorem monomial' {n : ℕ} (hn : n ≠ 0) (s : S) : HasSubst (monomial n s) :=
  HasSubst.monomial (Finsupp.single_ne_zero.mpr hn) s

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