monomial — Mathlib

English

If n is a finitely supported nonzero exponent function n : τ →₀ ℕ and s ∈ S, then the multivariate monomial MvPowerSeries.monomial n s admits substitution.

Русский

Если n — не нулевая функция степеней с конечной поддержкой, и s ∈ S, то многомерный мономиал MvPowerSeries.monomial n s допускает подстановку.

LaTeX

$$$\forall n : \tau \to_0 \mathbb{N},\ n \neq 0 \Rightarrow \forall s \in S,\ HasSubst\bigl(\mathrm{MvPowerSeries.monomial}(n,s)\bigr)$$$

Lean4

protected theorem monomial {n : τ →₀ ℕ} (hn : n ≠ 0) (s : S) : HasSubst (MvPowerSeries.monomial n s) := by
  classical
  apply HasSubst.of_constantCoeff_zero
  rw [← MvPowerSeries.coeff_zero_eq_constantCoeff, MvPowerSeries.coeff_monomial, if_neg hn.symm]

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